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  7361  tfindsg  7883  tfr3  8440  pssnn  9209  dfac5  10170  cfcoflem  10313  isf32lem12  10405  ltexprlem7  11083  dirtr  18648  erclwwlktr  30042  erclwwlkntr  30091  3cyclfrgrrn1  30305  frgrregord013  30415  chirredlem1  32410  mdsymlem4  32426  cdj3lem2b  32457  relpfrlem  44979  ssfz12  47331
  Copyright terms: Public domain W3C validator