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  7286  tfindsg  7803  tfr3  8330  pssnn  9093  dfac5  10039  cfcoflem  10182  isf32lem12  10274  ltexprlem7  10953  dirtr  18525  erclwwlktr  30097  erclwwlkntr  30146  3cyclfrgrrn1  30360  frgrregord013  30470  chirredlem1  32465  mdsymlem4  32481  cdj3lem2b  32512  relpfrlem  45190  ssfz12  47556