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

Theorem com3l 75
Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
com3l  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )

Proof of Theorem com3l
StepHypRef Expression
1 com3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com3r 73 . 2  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
32com3r 73 1  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4l  78  imp3a  420  exp3acom3r  1360  prel12  3789  reusv3  4542  tfindsg  4651  sotri2  5072  relcoi1  5201  isofrlem  5837  oprabid  5882  frxp  6225  poxp  6227  reldmtpos  6242  sorpsscmpl  6288  tfrlem9  6401  tfr3  6415  oawordri  6548  odi  6577  omass  6578  undifixp  6852  isinf  7076  pssnn  7081  ordiso2  7230  ordtypelem7  7239  cantnf  7395  indcardi  7668  dfac2  7757  cfslb2n  7894  infpssrlem4  7932  axdc4lem  8081  zorn2lem7  8129  fpwwe2lem8  8259  grudomon  8439  distrlem5pr  8651  ltexprlem1  8660  axpre-sup  8791  bndndx  9964  uzind2  10104  difreicc  10767  leexp1a  11160  unbenlem  12955  infpnlem1  12957  neindisj2  16860  cmpsub  17127  grpomndo  21013  rngoueqz  21097  shscli  21896  mdbr3  22877  mdbr4  22878  dmdbr3  22885  dmdbr4  22886  mdslmd1i  22909  chjatom  22937  mdsymlem4  22986  cdj3lem2b  23017  3jaodd  24065  dfon2lem6  24144  poseq  24253  nocvxminlem  24344  funray  24763  imgfldref2  25064  prj1b  25079  prj3  25080  inttrp  25108  eqfnung2  25118  cbcpcp  25162  supwlub  25274  dfps2  25289  latdir  25295  resgcom  25351  grpodivone  25373  ltrooo  25404  rngoridfz  25437  mvecrtol2  25477  muldisc  25481  svli2  25484  svs2  25487  unint2t  25518  nsn  25530  cmptdst  25568  limptlimpr2lem1  25574  limptlimpr2lem2  25575  islimrs4  25582  bwt2  25592  lvsovso  25626  cnegvex2  25660  rnegvex2  25661  addcanrg  25667  negveud  25668  negveudr  25669  subaddv  25671  clsmulcv  25682  distmlva  25688  distsava  25689  intvconlem1  25703  hdrmp  25706  mrdmcd  25794  cmpassoh  25801  cmpmon  25815  icmpmon  25816  eltintpar  25899  cmpmor  25975  setiscat  25979  clscnc  26010  pgapspf2  26053  lineval5a  26088  lineval6a  26089  iscol3  26094  isibg1a6  26125  lppotos  26144  nbssntrs  26147  pdiveql  26168  imp5p  26220  brabg2  26366  neificl  26467  frgra3vlem1  28178  3vfriswmgralem  28182  bnj517  28917
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator