Metamath Proof Explorer

Theorem mdandyvr14

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

Proof

Step Hyp Ref Expression
1 mdandyvr14.1 ⊢ φ ↔ ζ
2 mdandyvr14.2 ⊢ ψ ↔ σ
3 mdandyvr14.3 ⊢ χ ↔ φ
4 mdandyvr14.4 ⊢ θ ↔ ψ
5 mdandyvr14.5 ⊢ τ ↔ ψ
6 mdandyvr14.6 ⊢ η ↔ ψ
7 2 1 3 4 5 6 mdandyvr1 ⊢ χ ↔ ζ ∧ θ ↔ σ ∧ τ ↔ σ ∧ η ↔ σ