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

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  95  com24  96  isofrlem  7328  tfindsg  7845  tfr3  8374  pssnn  9141  dfac5  10100  cfcoflem  10244  isf32lem12  10336  ltexprlem7  11015  dirtr  18646  erclwwlktr  30278  erclwwlkntr  30327  3cyclfrgrrn1  30541  frgrregord013  30651  chirredlem1  32647  mdsymlem4  32663  cdj3lem2b  32694  relpfrlem  45521  ssfz12  47907