Metamath Proof Explorer


Theorem mdandyvr0

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

Proof

Step Hyp Ref Expression
1 mdandyvr0.1 ( 𝜑𝜁 )
2 mdandyvr0.2 ( 𝜓𝜎 )
3 mdandyvr0.3 ( 𝜒𝜑 )
4 mdandyvr0.4 ( 𝜃𝜑 )
5 mdandyvr0.5 ( 𝜏𝜑 )
6 mdandyvr0.6 ( 𝜂𝜑 )
7 3 1 bitri ( 𝜒𝜁 )
8 4 1 bitri ( 𝜃𝜁 )
9 7 8 pm3.2i ( ( 𝜒𝜁 ) ∧ ( 𝜃𝜁 ) )
10 5 1 bitri ( 𝜏𝜁 )
11 9 10 pm3.2i ( ( ( 𝜒𝜁 ) ∧ ( 𝜃𝜁 ) ) ∧ ( 𝜏𝜁 ) )
12 6 1 bitri ( 𝜂𝜁 )
13 11 12 pm3.2i ( ( ( ( 𝜒𝜁 ) ∧ ( 𝜃𝜁 ) ) ∧ ( 𝜏𝜁 ) ) ∧ ( 𝜂𝜁 ) )