Metamath Proof Explorer

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 ⊢ η