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	⊢ ( 𝜒 ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) → ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) ∧ ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) )
	plcofph.2	⊢ 𝜑
	plcofph.3	⊢ 𝜓
Assertion	plcofph	⊢ 𝜒

Proof

Step	Hyp	Ref	Expression
1		plcofph.1	⊢ ( 𝜒 ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) → ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) ∧ ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) )
2		plcofph.2	⊢ 𝜑
3		plcofph.3	⊢ 𝜓
4		pm3.24	⊢ ¬ ( 𝜑 ∧ ¬ 𝜑 )
5	2 4	pm3.2i	⊢ ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) )
6	5	a1i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) → ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) )
7	6 5	pm3.2i	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) → ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) ∧ ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) )
8	1	bicomi	⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) → ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) ∧ ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) ↔ 𝜒 )
9	8	biimpi	⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) → ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) ∧ ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) → 𝜒 )
10	7 9	ax-mp	⊢ 𝜒