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