Theorem plvcofph

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

	Ref	Expression
Hypotheses	plvcofph.1	⊢ ( 𝜒 ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) → ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) ∧ ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) )
	plvcofph.2	⊢ ( 𝜏 ↔ ( ( 𝜒 → 𝜃 ) ∧ ( 𝜑 ↔ 𝜒 ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜓 ↔ 𝜃 ) ) ) )
	plvcofph.3	⊢ ( 𝜂 ↔ ( 𝜒 ∧ 𝜏 ) )
	plvcofph.4	⊢ 𝜑
	plvcofph.5	⊢ 𝜓
	plvcofph.6	⊢ 𝜃
Assertion	plvcofph	⊢ 𝜂

Proof

Step	Hyp	Ref	Expression
1		plvcofph.1	⊢ ( 𝜒 ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) → ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) ∧ ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) )
2		plvcofph.2	⊢ ( 𝜏 ↔ ( ( 𝜒 → 𝜃 ) ∧ ( 𝜑 ↔ 𝜒 ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜓 ↔ 𝜃 ) ) ) )
3		plvcofph.3	⊢ ( 𝜂 ↔ ( 𝜒 ∧ 𝜏 ) )
4		plvcofph.4	⊢ 𝜑
5		plvcofph.5	⊢ 𝜓
6		plvcofph.6	⊢ 𝜃
7	1 4 5	plcofph	⊢ 𝜒
8	2 4 5 7 6	pldofph	⊢ 𝜏
9	7 8	pm3.2i	⊢ ( 𝜒 ∧ 𝜏 )
10	3	bicomi	⊢ ( ( 𝜒 ∧ 𝜏 ) ↔ 𝜂 )
11	10	biimpi	⊢ ( ( 𝜒 ∧ 𝜏 ) → 𝜂 )
12	9 11	ax-mp	⊢ 𝜂