Metamath Proof Explorer

Theorem mdandyvr0

Description: Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016)

Ref Expression
Hypotheses mdandyvr0.1 ⊢ φ ↔ ζ
mdandyvr0.2 ⊢ ψ ↔ σ
mdandyvr0.3 ⊢ χ ↔ φ
mdandyvr0.4 ⊢ θ ↔ φ
mdandyvr0.5 ⊢ τ ↔ φ
mdandyvr0.6 ⊢ η ↔ φ
Assertion mdandyvr0 ⊢ χ ↔ ζ ∧ θ ↔ ζ ∧ τ ↔ ζ ∧ η ↔ ζ

Proof

Step Hyp Ref Expression
1 mdandyvr0.1 ⊢ φ ↔ ζ
2 mdandyvr0.2 ⊢ ψ ↔ σ
3 mdandyvr0.3 ⊢ χ ↔ φ
4 mdandyvr0.4 ⊢ θ ↔ φ
5 mdandyvr0.5 ⊢ τ ↔ φ
6 mdandyvr0.6 ⊢ η ↔ φ
7 3 1 bitri ⊢ χ ↔ ζ
8 4 1 bitri ⊢ θ ↔ ζ
9 7 8 pm3.2i ⊢ χ ↔ ζ ∧ θ ↔ ζ
10 5 1 bitri ⊢ τ ↔ ζ
11 9 10 pm3.2i ⊢ χ ↔ ζ ∧ θ ↔ ζ ∧ τ ↔ ζ
12 6 1 bitri ⊢ η ↔ ζ
13 11 12 pm3.2i ⊢ χ ↔ ζ ∧ θ ↔ ζ ∧ τ ↔ ζ ∧ η ↔ ζ