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

Theorem com12 27
Description: Inference that swaps (commutes) antecedents in an implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com12.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
com12  |-  ( ps 
->  ( ph  ->  ch ) )

Proof of Theorem com12
StepHypRef Expression
1 id 19 . 2  |-  ( ps 
->  ps )
2 com12.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5com 26 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl5  28  syl6com  31  mpcom  32  syli  33  pm2.27  35  pm2.43b  46  syl9r  67  com3r  73  pm2.86i  92  pm2.24  100  con3rr3  126  expt  146  jad  152  pm2.61  161  syl5ibcom  209  syl5ibrcom  211  pm5.501  328  jaod  367  orel1  369  pm2.62  396  impcom  416  imp3a  417  expcom  421  exp3a  422  pm3.21  429  imdistanri  665  pm2.64  724  pm2.75  782  ccased  875  dedlem0b  881  3impd  1124  3expd  1127  mp3an1i  1228  simplbi2com  1309  meredith  1313  ax12olem21  1558  ax12olem23  1560  ax10lem16  1568  ax10lem26  1578  ax10  1580  hbimd  1673  19.21t  1676  equtrr  1694  sbequ2  1748  ax11b  1794  sb6rf  1836  sb56  1842  exmoeu  1996  moimv  2002  eupickbi  2020  2eu1  2034  exists2  2044  r19.12  2383  2gencl  2508  3gencl  2509  rcla4cv  2563  ceqex  2578  mob  2635  euind  2640  reuind  2654  sseq2  2841  uneqdifeq  3163  difsn  3368  eqsn  3386  preq12b  3399  intab  3498  iinss2  3559  trint0  3700  dtru  3768  sspwb  3788  copsexg  3816  pocl  3882  pofun  3891  solin  3898  frss  3921  tz7.7  3979  ordtri3  3989  ordtr2  3997  suc11  4055  onssneli  4061  eusv2  4105  ralxfrALT  4129  iunpw  4147  ordom  4242  limom  4248  peano5  4256  2optocl  4358  3optocl  4359  ssrel  4369  ssrelrel  4379  relop  4426  xpidtr  4656  trin2  4657  sotri3  4664  poltletr  4669  xp11  4702  relcnvtr  4782  funmo  4811  fss  4935  fv3  5070  tz6.12-1  5073  tz6.12c  5077  tz6.12i  5078  mpteqb  5140  fornex  5209  funfvima  5275  fvclss  5282  f1fveq  5307  isotr  5347  isotrALT  5348  isoselem  5353  oprabid  5394  ovg  5491  poxp  5722  soxp  5723  tposfn2  5749  sorpsscmpl  5777  iotaval  5791  onnseq  5826  smores  5834  smoel  5842  smogt  5849  smoiso2  5851  tfrlem2  5857  tfr3  5880  tz7.48-2  5919  tz7.48-3  5921  tz7.49  5922  abianfp  5936  oecl  6001  oaordex  6021  oalimcl  6023  oaass  6024  omordi  6029  omlimcl  6041  odi  6042  omeulem1  6045  oen0  6049  oewordri  6055  nnawordi  6084  nnaass  6085  nnmordi  6094  omabs  6110  omsmolem  6116  iiner  6196  2ecoptocl  6204  3ecoptocl  6205  th3qlem2  6220  undifixp  6300  xpdom2  6404  xpf1o  6517  infensuc  6533  php  6539  onomeneq  6544  isinf  6569  findcard2  6591  unblem2  6603  finsschain  6654  marypha1  6679  supub  6700  suplub  6701  supsnALT  6716  hartogs  6752  card2on  6761  card2inf  6762  xpwdomg  6792  elirrv  6804  inf3lem1  6822  inf3lem2  6823  inf3lem3  6824  inf3lem5  6826  noinfep  6853  noinfepOLD  6854  trcl  6903  en3lp  6911  tcel  6923  r1sdom  6939  rankonidlem  6992  rankxpsuc  7044  scottex  7047  pr2ne  7127  dif1card  7130  fodomnum  7176  cardaleph  7208  cflim2  7362  cfsmolem  7369  infpssrlem3  7404  isfin7-2  7495  fin1a2lem6  7504  fin1a2lem10  7508  fin1a2lem12  7510  domtriomlem  7541  axdc3lem4  7552  axdc4lem  7554  kmlem4  7592  kmlem9  7597  kmlem12  7600  kmlem13  7601  zorn2lem3  7611  zorn2lem4  7612  zorn2lem5  7613  zorn2lem6  7614  zorn2lem7  7615  zornn0g  7618  axdclem  7632  axdclem2  7633  ondomon  7669  alephval2  7676  cfpwsdom  7688  axrepnd  7698  tskr1om  7823  grupr  7851  gruiun  7853  ingru  7868  grothomex  7882  indpi  7962  nqereu  7984  genpnnp  8060  prlem934  8088  ltaddpr2  8090  reclem2pr  8103  mulgt0sr  8158  supsrlem  8164  lemul1a  9002  squeeze0  9051  peano5nni  9140  nnunb  9349  fzind  9497  nn0ind-raph  9500  zindd  9501  eluzadd  9644  uzin  9648  xmulasslem  9992  icoshft  10142  fzen  10193  expcllem  10488  expeq0  10506  mulexp  10515  leexp2r  10533  bernneq  10600  facdiv  10673  hashmap  10759  cjexp  10849  absexp  11001  iseraltlem2  11366  sin01gt0  11673  alzdvds  11780  dvdslegcd  11820  gcdneg  11830  rplpwr  11860  qredeq  11910  prmpwdvds  12076  prmreclem4  12091  ramcl  12201  imasleval  12548  mreiincl  12601  drsdirfi  12653  spwmo  12907  efgi2  13764  fiinopn  15374  tgcl  15434  distop  15460  isclo2  15551  iscldtop  15558  ssnei2  15579  opnnei  15583  pnfnei  15662  mnfnei  15663  tgcnp  15695  cnpnei  15705  2ndcctbss  15889  1stcelcls  15895  txcnpi  16010  cnmptcom  16080  fbfinnfr  16244  isfildlem  16260  snfil  16267  fbunfip  16272  fgcl  16281  elfm2  16351  fmfnfmlem1  16357  fmco  16364  fbflim2  16380  flffbas  16398  cnpflf2  16403  flimfcls  16429  tmdgsum  16486  xmeteq0  16611  neibl  16756  metcnp3  16795  fgcfil  17398  caubl  17434  volsuplem  17613  dvnadd  17955  dvnres  17956  cpnord  17960  mpfrcl  18068  ply1divex  18186  cxpmul2  18647  wilthlem3  18883  lgsquad2lem2  19173  qabvexp  19350  gxnn0add  19497  gxnn0mul  19500  ismgm  19543  isexid2  19548  rngodm1dm2  19641  ipassi  19975  ubthlem2  20006  isch3  20377  shintcli  20464  shmodsi  20524  spansncvi  20805  pjjsi  20853  hoaddsub  20952  eigorthi  20973  pjss2coi  21300  pjnormssi  21304  pj3cor1i  21345  strb  21394  dmdmd  21436  mdsl0  21446  csmdsymi  21470  chrelat2i  21501  cvati  21502  mdsymlem3  21541  mdsymlem6  21544  sumdmdlem2  21555  dmdbr5ati  21558  cvmlift2lem1  21730  3ccased  21973  dedekind  21977  dfres3  22009  dfon2lem3  22032  rdgprc  22042  trpredmintr  22126  trpredrec  22133  wfr3g  22147  wfrlem12  22159  frr3g  22172  frrlem11  22185  sltval2  22201  axfelem13  22250  elfuns  22352  axcontlem4  22493  cgrextend  22529  btwndiff  22548  btwnconn1lem12  22619  brsegle  22629  broutsideof2  22643  funray  22661  meran1  22723  waj-ax  22726  arg-ax  22728  wl-pm2.86i  22794  copsexgb  22831  evpexun  22859  isunscov  22911  restidsing  22913  twsymr  22915  prj1b  22916  prj3  22917  fixpc  22931  domintrefc  22963  mapmapmap  22987  injsurinj  22988  repfuntw  22999  cbcpcp  23001  prl  23006  prl2  23008  prjmapcp2  23009  dstr  23010  jidd  23031  midd  23032  int2pre  23076  ubpar  23100  inposet  23117  tolat  23125  toplat  23129  latdir  23134  ridlideq  23174  rzrlzreq  23175  resgcom  23190  grpodivone  23212  grpodivfo  23213  rltrran  23253  zerdivemp1  23275  zintdom  23277  muldisc  23323  svli2  23326  svs2  23329  truni1  23347  truni2  23348  truni3  23349  inttop2  23360  npmp  23366  nsn  23375  intopcoaconlem3b  23383  intopcoaconc  23386  qusp  23387  intcont  23388  prcnt  23396  fisub  23399  cmptdst  23413  exopcopn  23417  prdnei  23418  limptlimpr2lem1  23419  limptlimpr2lem2  23420  islimrs  23425  islimrs3  23426  islimrs4  23427  bwt2  23437  iintlem1  23455  iint  23457  lvsovso  23471  supnuf  23474  claddrvr  23493  sigadd  23494  addcomv  23500  addcanrg  23512  negveudr  23514  subclrvd  23519  distsava  23534  intvconlem1  23548  hdrmp  23551  cmppfd  23590  domcmpd  23591  codcmpd  23592  cmpasso  23618  cmpida  23619  cmpidb  23620  cmpassoh  23646  homgrf  23647  imonclem  23658  cmpmon  23660  iepiclem  23668  isepic  23669  idfisf  23686  issrc  23712  propsrc  23713  partarelt1  23741  inttaror  23745  inttarcar  23746  fnctartar  23752  fnctartar2  23753  prismorcset2  23763  cmpmor  23820  setiscat  23824  lemindclsbu  23841  indcls2  23842  clscnc  23856  pgapspf2  23899  lineval5a  23931  lineval6a  23932  isconcl5a  23945  isconcl5ab  23946  isconcl6a  23947  isibg2aa  23956  isib2g1a1  23960  isibg1a2  23961  isibg2a  23962  isibg1a3a  23966  isibg1a4a  23967  isibg1a5a  23968  bsstr  23972  nbssntr  23973  sgplpte21d  23980  segline  23985  pxysxy  23986  lppotoslem  23987  lppotos  23988  xsyysx  23989  nbssntrs  23991  pdiveql  24011  elicc3  24057  nn0prpwlem  24067  nn0prpw  24068  fnessref  24122  neibastop2lem  24138  filnetlem4  24159  fzmul  24273  fdc  24285  seqpo  24287  incsequz  24288  isismty  24355  ismtybndlem  24360  heibor1lem  24363  ghomco  24403  zerdivemp1x  24416  pridlc  24526  ceqsex3OLD  24556  nelss  24581  incssnn0  24618  fphpd  24728  jm2.19lem3  24913  setindtr  24946  dfac21  24997  aalioulem2  25011  islssfg2  25041  mpaaeu  25227  psgnunilem4  25292  pm14.24  25508  hirstL-ax3  25561  sb5ALT  25655  truniALT  25672  onfrALTlem3  25676  ee223  25765  3orbi123VD  25928  sbc3orgVD  25929  exbirVD  25931  exbiriVD  25932  sbcim2gVD  25953  trsbcVD  25955  truniALTVD  25956  onfrALTlem3VD  25965  onfrALTlem2VD  25967  csbrngVD  25974  19.41rgVD  25980  a9e2eqVD  25985  a9e2ndeqVD  25987  2uasbanhVD  25989  sb5ALTVD  25991  vk15.4jVD  25992  ax12-3  27509  ax9lem2  27546  ax9lem5  27549  ax9lem15  27559  ax9vax9  27563  cdleme18d  28889  tendovalco  29359  cdlemn11pre  29805  dihord2pre  29820
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator