Theorem plvcofphax

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

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

Proof

Step	Hyp	Ref	Expression
1		plvcofphax.1	⊢ ( 𝜒 ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) → ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) ∧ ( 𝜑 ∧ ¬ ( 𝜑 ∧ ¬ 𝜑 ) ) ) )
2		plvcofphax.2	⊢ ( 𝜏 ↔ ( ( 𝜒 → 𝜃 ) ∧ ( 𝜑 ↔ 𝜒 ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜓 ↔ 𝜃 ) ) ) )
3		plvcofphax.3	⊢ ( 𝜂 ↔ ( 𝜒 ∧ 𝜏 ) )
4		plvcofphax.4	⊢ 𝜑
5		plvcofphax.5	⊢ 𝜓
6		plvcofphax.6	⊢ 𝜃
7		plvcofphax.7	⊢ ( 𝜁 ↔ ¬ ( 𝜓 ∧ ¬ 𝜏 ) )
8	1 4 5	plcofph	⊢ 𝜒
9	2 4 5 8 6	pldofph	⊢ 𝜏
10	5 9	pm3.2i	⊢ ( 𝜓 ∧ 𝜏 )
11		pm3.4	⊢ ( ( 𝜓 ∧ 𝜏 ) → ( 𝜓 → 𝜏 ) )
12	10 11	ax-mp	⊢ ( 𝜓 → 𝜏 )
13		iman	⊢ ( ( 𝜓 → 𝜏 ) ↔ ¬ ( 𝜓 ∧ ¬ 𝜏 ) )
14	13	biimpi	⊢ ( ( 𝜓 → 𝜏 ) → ¬ ( 𝜓 ∧ ¬ 𝜏 ) )
15	12 14	ax-mp	⊢ ¬ ( 𝜓 ∧ ¬ 𝜏 )
16	7	bicomi	⊢ ( ¬ ( 𝜓 ∧ ¬ 𝜏 ) ↔ 𝜁 )
17	16	biimpi	⊢ ( ¬ ( 𝜓 ∧ ¬ 𝜏 ) → 𝜁 )
18	15 17	ax-mp	⊢ 𝜁