Theorem plcofph 41111

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

Hypotheses

Ref	Expression
plcofph.1	|- ( ch <-> ( ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) ) /\ ( ph /\ -. ( ph /\ -. ph ) ) ) )
plcofph.2	|- ph
plcofph.3	|- ps

Assertion

Ref	Expression
plcofph	|- ch

Proof of Theorem plcofph

Step	Hyp	Ref	Expression
1		plcofph.2	. . . . 5 |- ph
2		pm3.24 926	. . . . 5 |- -. ( ph /\ -. ph )
3	1, 2	pm3.2i 471	. . . 4 |- ( ph /\ -. ( ph /\ -. ph ) )
4	3	a1i 11	. . 3 |- ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) )
5	4, 3	pm3.2i 471	. 2 |- ( ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) ) /\ ( ph /\ -. ( ph /\ -. ph ) ) )
6		plcofph.1	. . . 4 |- ( ch <-> ( ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) ) /\ ( ph /\ -. ( ph /\ -. ph ) ) ) )
7	6	bicomi 214	. . 3 |- ( ( ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) ) /\ ( ph /\ -. ( ph /\ -. ph ) ) ) <-> ch )
8	7	biimpi 206	. 2 |- ( ( ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) ) /\ ( ph /\ -. ( ph /\ -. ph ) ) ) -> ch )
9	5, 8	ax-mp 5	1 |- ch

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

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

This theorem is referenced by:  plvcofph  41113  plvcofphax  41114