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