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

Theorem com4t 90
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 89 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
32com4l 89 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  91  com24  92  isofrlem  6465  tfindsg  6926  tfr3  7356  pssnn  8037  dfac5  8808  cfcoflem  8951  isf32lem12  9043  ltexprlem7  9717  dirtr  17002  erclwwlktr  26106  erclwwlkntr  26118  el2wlkonot  26159  3cyclfrgrarn1  26302  frgraregord013  26408  chirredlem1  28436  mdsymlem4  28452  cdj3lem2b  28483  ssfz12  40175  erclwwlkstr  41242  erclwwlksntr  41254  3cyclfrgrrn1  41454  av-frgraregord013  41548
  Copyright terms: Public domain W3C validator