Theorem plvcofphax 44329

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

Hypotheses

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

Assertion

Ref	Expression
plvcofphax	⊢ 𝜁

Proof of Theorem plvcofphax

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by: (None)