Metamath Proof Explorer

Theorem mdandyvr7

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 mdandyvr7.1 ⊢ φ ↔ ζ
mdandyvr7.2 ⊢ ψ ↔ σ
mdandyvr7.3 ⊢ χ ↔ ψ
mdandyvr7.4 ⊢ θ ↔ ψ
mdandyvr7.5 ⊢ τ ↔ ψ
mdandyvr7.6 ⊢ η ↔ φ
Assertion mdandyvr7 ⊢ χ ↔ σ ∧ θ ↔ σ ∧ τ ↔ σ ∧ η ↔ ζ

Proof

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