Theorem com4t 93

Description: Commutation of antecedents. Rotate twice. (Contributed by NM, 25-Apr-1994.)

Hypothesis

Ref	Expression
com4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
com4t	⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))

Proof of Theorem com4t

Step	Hyp	Ref	Expression
1		com4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	com4l 92	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	com4l 92	1 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com4r  94  com24  95  isofrlem  7281  tfindsg  7801  tfr3  8328  pssnn  9092  dfac5  10042  cfcoflem  10185  isf32lem12  10277  ltexprlem7  10955  dirtr  18526  erclwwlktr  29984  erclwwlkntr  30033  3cyclfrgrrn1  30247  frgrregord013  30357  chirredlem1  32352  mdsymlem4  32368  cdj3lem2b  32399  relpfrlem  44927  ssfz12  47299