Metamath Proof Explorer

Theorem mdandyvr3

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

Proof

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