Proof - ta1pm:

(pvp)	;
p	; t--80

 Proof - ta2pm:

q	;
a + c	; t--37
=> a + b + c	; introduce
(pvq)	; d--12

 Proof - ta2pm_1:

(q => (pvq))	;
(q&(pvq)) / q	; t--59
(q + (pvq) - (qvpvq)) / q	; t--68
(q + (pvq) - (pvqvq)) / q	; t--75
(q + (pvq) - (pvq)) / q	; t--80
q / q	; reduce
1	; reduce

 Proof - ta3pm_1:

(pvq) => (qvp)	;
((pvq)&(qvp)) / (pvq)	; t--59
((pvq) + (qvp) - ((pvq)v(qvp))) / (pvq)	; t--68
((pvq) + (pvq) - ((pvq)v(pvq))) / (pvq)	; t--75, t--75
((pvq) + (pvq) - (pvq)) / (pvq)	; t--80
(pvq) / (pvq)	; reduce
1	; reduce

 Proof - ta3pm:

(pvq)	;
(qvp)	; t--75

 Proof - ta4pm:

((pvq) => (pvr))	;
((pvq)&(pvr)) / (pvq)	; t--59
(pv(q&r)) / (pvq)	; t--173
(p + (q&r) - (p&q&r)) / (pvq)	; t--61
((a+b) + (e+g) - e) / (pvq)	; t--34, t--160, d--144
(a + b + g) / (pvq)	; reduce
(a + b + g) / (a + b + c)	; d--12
(a + b + g) / (a + b + g + k)	; d--142
(e + i + f + j + g) / (e + i + f + j + g + k)	; d--140, d--141, d--140, d--141
(q => r)	;
(q&r) / q	; t--59
(e+g) / (a+c)	; t--160, t--37
(e + g) / (e + i + g + k)	; d--140, d--142
=> (e + i + f + j + g) / (e + i + f + j + g + k)	; introduce
((pvq) => (pvr))	;

 No proof available - t:

;
;
(p -> (p&q))	(p -> q)	;
(p <-> (p&q))	(p -> q)	;
(p = (p&q))	T(p -> q)	;
(p (p&q))	L(p -> q)	;
	;
(p => (p&q))	(p => q)	;
(p <=> (p&q))	(p => q)	;
T(p => (p&q))	T(p => q)	;
L(p => (p&q))	L(p => q)	;
;
((pvq) -> (p&q))	(p <-> q)	;
((pvq) <-> (p&q))	(p <-> q)	;
((pvq) = (p&q))	T(p <-> q)	;
((pvq) (p&q))	L(p <-> q)	;
	;
((pvq) => (p&q))	(p <=> q)	;
((pvq) <=> (p&q))	(p <=> q)	;
T((pvq) => (p&q))	T(p <=> q)	;
L((pvq) => (p&q))	L(p <=> q)	;
;
;
;
;
;