Metamath Proof Explorer

Theorem mdandyvr4

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

Proof

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