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

Theorem com4t 85
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 84 . 2
32com4l 84 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  com4r  86  com24  87  mopickOLD  2357  isofrlem  6236  tfindsg  6695  tfr3  7087  pssnn  7758  dfac5  8530  cfcoflem  8673  isf32lem12  8765  ltexprlem7  9441  dirtr  15866  erclwwlktr  24815  erclwwlkntr  24827  el2wlkonot  24869  3cyclfrgrarn1  25012  frgraregord013  25118  chirredlem1  27309  mdsymlem4  27325  cdj3lem2b  27356  ssfz12  32330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator