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  7296  tfindsg  7813  tfr3  8340  pssnn  9105  dfac5  10051  cfcoflem  10194  isf32lem12  10286  ltexprlem7  10965  dirtr  18537  erclwwlktr  30109  erclwwlkntr  30158  3cyclfrgrrn1  30372  frgrregord013  30482  chirredlem1  32477  mdsymlem4  32493  cdj3lem2b  32524  relpfrlem  45303  ssfz12  47668