Theorem plvcofph 47960

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

Hypotheses

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

Assertion

Ref	Expression
plvcofph	⊢ 𝜂

Proof of Theorem plvcofph

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by: (None)