Theorem plvcofph

Description: Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020)

	Ref	Expression
Hypotheses	plvcofph.1	|- ( ch <-> ( ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) ) /\ ( ph /\ -. ( ph /\ -. ph ) ) ) )
	plvcofph.2	|- ( ta <-> ( ( ch -> th ) /\ ( ph <-> ch ) /\ ( ( ph -> ps ) -> ( ps <-> th ) ) ) )
	plvcofph.3	|- ( et <-> ( ch /\ ta ) )
	plvcofph.4	|- ph
	plvcofph.5	|- ps
	plvcofph.6	|- th
Assertion	plvcofph	|- et

Proof

Step	Hyp	Ref	Expression
1		plvcofph.1	|- ( ch <-> ( ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) ) /\ ( ph /\ -. ( ph /\ -. ph ) ) ) )
2		plvcofph.2	|- ( ta <-> ( ( ch -> th ) /\ ( ph <-> ch ) /\ ( ( ph -> ps ) -> ( ps <-> th ) ) ) )
3		plvcofph.3	|- ( et <-> ( ch /\ ta ) )
4		plvcofph.4	|- ph
5		plvcofph.5	|- ps
6		plvcofph.6	|- th
7	1 4 5	plcofph	|- ch
8	2 4 5 7 6	pldofph	|- ta
9	7 8	pm3.2i	|- ( ch /\ ta )
10	3	bicomi	|- ( ( ch /\ ta ) <-> et )
11	10	biimpi	|- ( ( ch /\ ta ) -> et )
12	9 11	ax-mp	|- et