Metamath Proof Explorer

Theorem mdandyvr11

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

Proof

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