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  7349  tfindsg  7866  tfr3  8395  pssnn  9163  dfac5  10131  cfcoflem  10274  isf32lem12  10366  ltexprlem7  11045  dirtr  18683  erclwwlktr  30410  erclwwlkntr  30459  3cyclfrgrrn1  30673  frgrregord013  30783  chirredlem1  32779  mdsymlem4  32795  cdj3lem2b  32826  relpfrlem  45703  ssfz12  48092