Theorem com4t 91

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 90	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	com4l 90	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  92  com24  93  isofrlem  6490  tfindsg  6952  tfr3  7382  pssnn  8063  dfac5  8834  cfcoflem  8977  isf32lem12  9069  ltexprlem7  9743  dirtr  17059  erclwwlktr  26343  erclwwlkntr  26355  el2wlkonot  26396  3cyclfrgrarn1  26539  frgraregord013  26645  chirredlem1  28633  mdsymlem4  28649  cdj3lem2b  28680  ssfz12  40351  erclwwlkstr  41243  erclwwlksntr  41255  3cyclfrgrrn1  41455  av-frgraregord013  41549