Theorem com4t 94

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 93	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	com4l 93	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  95  com24  96  isofrlem  7340  tfindsg  7858  tfr3  8387  pssnn  9154  dfac5  10113  cfcoflem  10257  isf32lem12  10349  ltexprlem7  11028  dirtr  18659  erclwwlktr  30354  erclwwlkntr  30403  3cyclfrgrrn1  30617  frgrregord013  30727  chirredlem1  32723  mdsymlem4  32739  cdj3lem2b  32770  relpfrlem  45645  ssfz12  48034