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

Theorem com12 29
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 20 . 2  |-  ( ps 
->  ps )
2 com12.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5com 28 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl5  30  syl6com  33  mpcom  34  syli  35  pm2.27  37  pm2.43b  48  syl9r  69  com3r  75  pm2.86i  94  pm2.24  103  con3rr3  130  expt  150  jad  156  pm2.61  165  syl5ibcom  212  syl5ibrcom  214  pm5.501  331  jaod  370  orel1  372  pm2.62  399  impcom  420  imp3a  421  expcom  425  exp3a  426  pm3.21  436  imdistanri  673  pm2.64  765  pm2.75  823  ccased  914  dedlem0b  920  3impd  1167  3expd  1170  mp3an1i  1272  simplbi2com  1380  meredith  1410  sbequ2  1657  equtrr  1690  ax12olem3OLD  1967  ax10lem2  1979  ax10lem4OLD  1986  ax11b  2029  sb6rf  2124  sb56  2131  exsb  2164  mo  2260  exmoeu  2280  morimv  2286  eupickbi  2304  2mo  2316  2eu1  2318  exists2  2328  r19.12  2762  2gencl  2928  3gencl  2929  rspccv  2992  ceqex  3009  mob  3059  euind  3064  reuind  3080  2rmorex  3081  sseq2  3313  reupick2  3570  uneqdifeq  3659  difsn  3876  eqsn  3903  preq12b  3916  prnebg  3921  iinss2  4084  disjxiun  4150  trint0  4260  dtru  4331  sspwb  4354  copsexg  4383  pocl  4451  pofun  4460  solin  4467  frss  4490  tz7.7  4548  ordtri3  4558  ordtr2  4566  suc11  4625  onssneli  4631  reusv1  4663  reusv2lem1  4664  alxfr  4676  ralxfrALT  4682  iunpw  4699  ordom  4794  limom  4800  peano5  4808  2optocl  4893  3optocl  4894  ssrel  4904  ssrel2  4906  ssrelrel  4916  relop  4963  asymref2  5191  xpidtr  5196  trin2  5197  sotri3  5204  poltletr  5209  xp11  5244  relcnvtr  5329  iotaval  5369  funmo  5410  fss  5539  fv3  5684  tz6.12c  5690  tz6.12i  5691  mpteqb  5758  eldmrexrnb  5816  fornex  5909  funfvima  5912  fvclss  5919  f1veqaeq  5944  isoselem  6000  oprabid  6044  ovg  6151  bropopvvv  6365  poxp  6394  soxp  6395  mpt2xopoveqd  6408  tposfn2  6437  sorpsscmpl  6469  onnseq  6542  smoel  6558  smogt  6565  smoiso2  6567  tfrlem2  6573  tfr3  6596  tz7.48-2  6635  tz7.48-3  6637  tz7.49  6638  abianfp  6652  oecl  6717  oaordex  6737  oalimcl  6739  oaass  6740  omordi  6745  omlimcl  6757  odi  6758  omeulem1  6761  oen0  6765  oewordri  6771  nnawordi  6800  nnaass  6801  nnmordi  6810  omabs  6826  omsmolem  6832  iiner  6912  2ecoptocl  6931  3ecoptocl  6932  th3qlem2  6947  undifixp  7034  xpdom2  7139  xpf1o  7205  infensuc  7221  php  7227  onomeneq  7232  isinf  7258  findcard2  7284  unblem2  7296  finsschain  7348  marypha1  7374  hartogs  7446  card2on  7455  card2inf  7456  xpwdomg  7486  elirrv  7498  inf3lem1  7516  inf3lem2  7517  inf3lem3  7518  inf3lem5  7520  noinfep  7547  noinfepOLD  7548  trcl  7597  en3lp  7605  tcel  7617  r1sdom  7633  rankonidlem  7687  scottex  7742  pr2ne  7822  dif1card  7825  fodomnum  7871  cardaleph  7903  kmlem4  7966  kmlem9  7971  kmlem12  7974  kmlem13  7975  cflim2  8076  cfsmolem  8083  infpssrlem3  8118  isfin7-2  8209  fin1a2lem6  8218  fin1a2lem10  8222  fin1a2lem12  8224  domtriomlem  8255  axdc3lem4  8266  axdc4lem  8268  zorn2lem3  8311  zorn2lem4  8312  zorn2lem5  8313  zorn2lem6  8314  zorn2lem7  8315  zornn0g  8318  axdclem  8332  axdclem2  8333  ondomon  8371  alephval2  8380  cfpwsdom  8392  wunr1om  8527  wuncval2  8555  tskr1om  8575  grupr  8605  gruiun  8607  ingru  8623  grothomex  8637  indpi  8717  nqereu  8739  genpnnp  8815  prlem934  8843  ltaddpr2  8845  reclem2pr  8858  mulgt0sr  8913  supsrlem  8919  lemul1a  9796  squeeze0  9845  peano5nni  9935  nnunb  10149  fzind  10300  nn0ind-raph  10302  zindd  10303  eluzadd  10446  uzin  10450  xmulasslem  10796  icoshft  10951  fzen  11004  elfznelfzo  11119  injresinjlem  11126  injresinj  11127  expcllem  11319  expeq0  11337  mulexp  11346  leexp2r  11364  bernneq  11432  facdiv  11505  hasheqf1oi  11562  hashf1rn  11563  hashnn0n0nn  11591  hashle00  11596  hashgt12el  11609  hashgt12el2  11610  hash2prde  11615  hashtpg  11618  hashmap  11625  brfi1uzind  11642  cjexp  11882  absexp  12036  iseraltlem2  12403  sin01gt0  12718  alzdvds  12826  dvdslegcd  12943  gcdneg  12953  rplpwr  12983  qredeq  13033  prmpwdvds  13199  prmreclem4  13214  ramcl  13324  imasleval  13693  mreiincl  13748  mreexexd  13800  drsdirfi  14322  spwmo  14585  efgi2  15284  fiinopn  16897  tgcl  16957  distop  16983  isclo2  17075  iscldtop  17082  ssnei2  17103  opnnei  17107  pnfnei  17206  mnfnei  17207  tgcnp  17239  cnpnei  17250  2ndcctbss  17439  1stcelcls  17445  txcnpi  17561  cnmptcom  17631  fbfinnfr  17794  isfildlem  17810  snfil  17817  fbunfip  17822  fgcl  17831  elfm2  17901  fmfnfmlem1  17907  fmco  17914  fbflim2  17930  flffbas  17948  cnpflf2  17953  flimfcls  17979  tmdgsum  18046  neibl  18421  metcnp3  18460  fgcfil  19095  caubl  19131  volsuplem  19316  ellimc3  19633  dvnadd  19682  dvnres  19684  cpnord  19688  dvnfre  19705  mpfrcl  19806  ply1divex  19926  aalioulem2  20117  cxpmul2  20447  wilthlem3  20720  lgsquad2lem2  21010  qabvexp  21187  uhgraeq12d  21209  ausisusgra  21247  usgraeq12d  21252  usgraedgprv  21263  usgraedgrnv  21264  usgraedg4  21272  usgra1v  21275  usgraidx2v  21278  usgrafisinds  21293  nbgraop  21302  nbusgra  21306  nbgranself2  21314  nbgraf1olem1  21317  nbgraf1olem5  21321  nb3graprlem1  21326  cusgrarn  21334  nbcusgra  21338  cusgrasize2inds  21352  cusgrafi  21357  sizeusglecusglem1  21359  sizeusglecusg  21361  uvtxnbgra  21368  pthdepisspth  21428  1pthoncl  21440  constr2trl  21446  2pthoncl  21451  redwlk  21454  wlkdvspth  21456  cyclnspth  21466  cyclispthon  21468  fargshiftfo  21473  usgrcyclnl1  21475  nvnencycllem  21478  3v3e3cycl1  21479  constr3trllem2  21486  4cycl4v4e  21501  4cycl4dv  21502  4cycl4dv4e  21503  vdusgraval  21526  eupatrl  21538  gxnn0add  21710  gxnn0mul  21713  ismgm  21756  isexid2  21761  zerdivemp1  21870  ipassi  22190  ubthlem2  22221  isch3  22592  shintcli  22679  shmodsi  22739  spansncvi  23002  pjjsi  23050  hoaddsub  23167  eigorthi  23188  pjss2coi  23515  pjnormssi  23519  pj3cor1i  23560  strb  23609  dmdmd  23651  mdsl0  23661  csmdsymi  23685  chrelat2i  23716  cvati  23717  mdsymlem3  23756  mdsymlem6  23759  sumdmdlem2  23770  dmdbr5ati  23773  cvmlift2lem1  24768  3ccased  24955  dedekind  24966  clim2prod  24995  prodfn0  25001  prodfrec  25002  prodmo  25041  fprodabs  25076  fprodefsum  25077  dfres3  25140  dfon2lem3  25165  rdgprc  25175  trpredmintr  25258  trpredrec  25265  wfr3g  25279  wfrlem12  25291  frr3g  25304  frrlem11  25317  sltval2  25334  axcontlem4  25620  cgrextend  25656  btwndiff  25675  btwnconn1lem12  25746  brsegle  25756  broutsideof2  25770  funray  25788  meran1  25875  waj-ax  25878  arg-ax  25880  wl-pm2.86i  25945  elicc3  26011  nn0prpwlem  26016  nn0prpw  26017  fnessref  26064  neibastop2lem  26080  filnetlem4  26101  fzmul  26135  fdc  26140  seqpo  26142  incsequz  26143  isismty  26201  ismtybndlem  26206  heibor1lem  26209  ghomco  26249  zerdivemp1x  26262  pridlc  26372  ceqsex3OLD  26400  nelss  26423  incssnn0  26456  fphpd  26568  jm2.19lem3  26753  setindtr  26786  dfac21  26833  islssfg2  26838  mpaaeu  27024  psgnunilem4  27089  stoweidlem26  27443  hirstL-ax3  27528  rexsb  27614  rexrsb  27615  2reu1  27632  afvres  27705  tz6.12-afv  27706  afvco2  27709  ndmaovdistr  27740  frgraunss  27748  frgra2v  27752  frgra3vlem1  27753  frgra3vlem2  27754  3vfriswmgralem  27757  3vfriswmgra  27758  2pthfrgra  27764  3cyclfrgrarn1  27765  n4cyclfrgra  27771  frgranbnb  27773  vdn0frgrav2  27777  vdgn0frgrav2  27778  frgrancvvdeqlem2  27783  frgrancvvdeqlem3  27784  frgrancvvdeqlem4  27785  frgrancvvdeqlem7  27788  frgrancvvdeqlemA  27789  frgrancvvdeqlemB  27790  frgrancvvdeqlemC  27791  frgrawopreglem3  27798  frgrawopreglem4  27799  frgrawopreglem5  27800  frgrawopreg  27801  frgrawopreg1  27802  frgrawopreg2  27803  sb5ALT  27952  truniALT  27969  onfrALTlem3  27973  ee223  28076  3orbi123VD  28303  sbc3orgVD  28304  exbirVD  28306  exbiriVD  28307  sbcim2gVD  28328  trsbcVD  28330  truniALTVD  28331  onfrALTlem3VD  28340  onfrALTlem2VD  28342  csbrngVD  28349  19.41rgVD  28355  a9e2eqVD  28360  a9e2ndeqVD  28362  2uasbanhVD  28364  sb5ALTVD  28366  vk15.4jVD  28367  ax12olem3aAUX7  28795  ax10lem4NEW7  28809  sb6rfNEW7  28925  sb56NEW7  28929  exsbNEW7  28932  ax11bNEW7  28955  cdleme18d  30409  tendovalco  30879  cdlemn11pre  31325  dihord2pre  31340
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator