Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jarvin Udandy
mdandyvr12
Metamath Proof Explorer
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
⊢ ( ( ( ( 𝜒 ↔ 𝜁 ) ∧ ( 𝜃 ↔ 𝜁 ) ) ∧ ( 𝜏 ↔ 𝜎 ) ) ∧ ( 𝜂 ↔ 𝜎 ) )