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  7340  tfindsg  7861  tfr3  8391  pssnn  9168  dfac5  10188  cfcoflem  10331  isf32lem12  10423  ltexprlem7  11108  dirtr  18756  erclwwlktr  30595  erclwwlkntr  30644  3cyclfrgrrn1  30868  frgrregord013  30978  chirredlem1  32974  mdsymlem4  32990  cdj3lem2b  33021  relpfrlem  45895  ssfz12  48328