Theorem plvcofphax

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

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

Proof

Step	Hyp	Ref	Expression
1		plvcofphax.1	|- ( ch <-> ( ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) ) /\ ( ph /\ -. ( ph /\ -. ph ) ) ) )
2		plvcofphax.2	|- ( ta <-> ( ( ch -> th ) /\ ( ph <-> ch ) /\ ( ( ph -> ps ) -> ( ps <-> th ) ) ) )
3		plvcofphax.3	|- ( et <-> ( ch /\ ta ) )
4		plvcofphax.4	|- ph
5		plvcofphax.5	|- ps
6		plvcofphax.6	|- th
7		plvcofphax.7	|- ( ze <-> -. ( ps /\ -. ta ) )
8	1 4 5	plcofph	|- ch
9	2 4 5 8 6	pldofph	|- ta
10	5 9	pm3.2i	|- ( ps /\ ta )
11		pm3.4	|- ( ( ps /\ ta ) -> ( ps -> ta ) )
12	10 11	ax-mp	|- ( ps -> ta )
13		iman	|- ( ( ps -> ta ) <-> -. ( ps /\ -. ta ) )
14	13	biimpi	|- ( ( ps -> ta ) -> -. ( ps /\ -. ta ) )
15	12 14	ax-mp	|- -. ( ps /\ -. ta )
16	7	bicomi	|- ( -. ( ps /\ -. ta ) <-> ze )
17	16	biimpi	|- ( -. ( ps /\ -. ta ) -> ze )
18	15 17	ax-mp	|- ze