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 ⊢ ( ( ( ( 𝜒 ↔ 𝜎 ) ∧ ( 𝜃 ↔ 𝜎 ) ) ∧ ( 𝜏 ↔ 𝜁 ) ) ∧ ( 𝜂 ↔ 𝜎 ) )