Theorem plvcofphax 41114

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

Hypotheses

Ref	Expression
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

Ref	Expression
plvcofphax	|- ze

Proof of Theorem plvcofphax

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by: (None)