Metamath Proof Explorer

Theorem mdandyvr13

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

Proof

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