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  7374  tfindsg  7899  tfr3  8438  pssnn  9215  dfac5  10237  cfcoflem  10380  isf32lem12  10472  ltexprlem7  11157  dirtr  18808  erclwwlktr  30646  erclwwlkntr  30695  3cyclfrgrrn1  30919  frgrregord013  31029  chirredlem1  33025  mdsymlem4  33041  cdj3lem2b  33072  relpfrlem  46149  ssfz12  48599