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  7204  tfindsg  7695  tfr3  8214  pssnn  8916  pssnnOLD  9001  dfac5  9868  cfcoflem  10012  isf32lem12  10104  ltexprlem7  10782  dirtr  18301  erclwwlktr  28365  erclwwlkntr  28414  3cyclfrgrrn1  28628  frgrregord013  28738  chirredlem1  30731  mdsymlem4  30747  cdj3lem2b  30778  ssfz12  44758