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

Theorem com4t 93
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 92 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
32com4l 92 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  94  com24  95  isofrlem  7076  tfindsg  7559  tfr3  8022  pssnn  8724  dfac5  9543  cfcoflem  9687  isf32lem12  9779  ltexprlem7  10457  dirtr  17841  erclwwlktr  27810  erclwwlkntr  27859  3cyclfrgrrn1  28073  frgrregord013  28183  chirredlem1  30176  mdsymlem4  30192  cdj3lem2b  30223  ssfz12  43858
  Copyright terms: Public domain W3C validator