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  7361  tfindsg  7883  tfr3  8440  pssnn  9209  dfac5  10170  cfcoflem  10313  isf32lem12  10405  ltexprlem7  11083  dirtr  18648  erclwwlktr  30042  erclwwlkntr  30091  3cyclfrgrrn1  30305  frgrregord013  30415  chirredlem1  32410  mdsymlem4  32426  cdj3lem2b  32457  relpfrlem  44979  ssfz12  47331