Metamath Proof Explorer

Theorem mdandyvr10

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

Proof

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