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