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  7360  tfindsg  7882  tfr3  8438  pssnn  9207  dfac5  10167  cfcoflem  10310  isf32lem12  10402  ltexprlem7  11080  dirtr  18660  erclwwlktr  30051  erclwwlkntr  30100  3cyclfrgrrn1  30314  frgrregord013  30424  chirredlem1  32419  mdsymlem4  32435  cdj3lem2b  32466  ssfz12  47264
  Copyright terms: Public domain W3C validator