Metamath Proof Explorer


Theorem com35

Description: Commutation of antecedents. Swap 3rd and 5th. Deduction associated with com24 . Double deduction associated with com13 . (Contributed by Jeff Hankins, 28-Jun-2009)

Ref Expression
Hypothesis com5.1 ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜃 → ( 𝜏𝜂 ) ) ) ) )
Assertion com35 ( 𝜑 → ( 𝜓 → ( 𝜏 → ( 𝜃 → ( 𝜒𝜂 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 com5.1 ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜃 → ( 𝜏𝜂 ) ) ) ) )
2 1 com34 ( 𝜑 → ( 𝜓 → ( 𝜃 → ( 𝜒 → ( 𝜏𝜂 ) ) ) ) )
3 2 com45 ( 𝜑 → ( 𝜓 → ( 𝜃 → ( 𝜏 → ( 𝜒𝜂 ) ) ) ) )
4 3 com34 ( 𝜑 → ( 𝜓 → ( 𝜏 → ( 𝜃 → ( 𝜒𝜂 ) ) ) ) )