Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  com4t Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 com4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21com4l 90 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
32com4l 90 1 (𝜒 → (𝜃 → (𝜑 → (𝜓𝜏))))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator