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  7873  tfr3  8411  pssnn  9188  dfac5  10211  cfcoflem  10354  isf32lem12  10446  ltexprlem7  11131  dirtr  18782  erclwwlktr  30619  erclwwlkntr  30668  3cyclfrgrrn1  30892  frgrregord013  31002  chirredlem1  32998  mdsymlem4  33014  cdj3lem2b  33045  relpfrlem  46037  ssfz12  48478