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 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4r  95  com24  96  isofrlem  7345  tfindsg  7861  tfr3  8392  pssnn  9167  dfac5  10135  cfcoflem  10278  isf32lem12  10370  ltexprlem7  11055  dirtr  18696  erclwwlktr  30500  erclwwlkntr  30549  3cyclfrgrrn1  30773  frgrregord013  30883  chirredlem1  32879  mdsymlem4  32895  cdj3lem2b  32926  relpfrlem  45784  ssfz12  48210