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  6630  tfindsg  7102  tfr3  7540  pssnn  8219  dfac5  8989  cfcoflem  9132  isf32lem12  9224  ltexprlem7  9902  dirtr  17283  erclwwlktr  26979  erclwwlkntr  27035  3cyclfrgrrn1  27265  frgrregord013  27382  chirredlem1  29377  mdsymlem4  29393  cdj3lem2b  29424  ssfz12  41649
  Copyright terms: Public domain W3C validator