Metamath Proof Explorer


Theorem mdandyvr12

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 mdandyvr12.1 ( 𝜑𝜁 )
mdandyvr12.2 ( 𝜓𝜎 )
mdandyvr12.3 ( 𝜒𝜑 )
mdandyvr12.4 ( 𝜃𝜑 )
mdandyvr12.5 ( 𝜏𝜓 )
mdandyvr12.6 ( 𝜂𝜓 )
Assertion mdandyvr12 ( ( ( ( 𝜒𝜁 ) ∧ ( 𝜃𝜁 ) ) ∧ ( 𝜏𝜎 ) ) ∧ ( 𝜂𝜎 ) )

Proof

Step Hyp Ref Expression
1 mdandyvr12.1 ( 𝜑𝜁 )
2 mdandyvr12.2 ( 𝜓𝜎 )
3 mdandyvr12.3 ( 𝜒𝜑 )
4 mdandyvr12.4 ( 𝜃𝜑 )
5 mdandyvr12.5 ( 𝜏𝜓 )
6 mdandyvr12.6 ( 𝜂𝜓 )
7 2 1 3 4 5 6 mdandyvr3 ( ( ( ( 𝜒𝜁 ) ∧ ( 𝜃𝜁 ) ) ∧ ( 𝜏𝜎 ) ) ∧ ( 𝜂𝜎 ) )