Theorem plcofph

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

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

Proof

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