MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com12 Structured version   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  1383  meredith  1413  sbequ2  1660  sbequ2OLD  1661  equtrr  1695  cbv1  1973  ax12olem3OLD  2013  ax10lem2  2023  ax10lem4OLD  2030  dvelimdf  2070  ax11b  2082  equveli  2085  sbequi  2110  sbied  2150  sb6rf  2167  sb56  2174  exsb  2207  mo  2303  exmoeu  2323  morimv  2329  eupickbi  2347  2mo  2359  2eu1  2361  exists2  2371  r19.12  2819  2gencl  2985  3gencl  2986  rspccv  3049  ceqex  3066  mob  3116  euind  3121  reuind  3137  2rmorex  3138  sseq2  3370  reupick2  3627  uneqdifeq  3716  difsn  3933  eqsn  3960  preq12b  3974  prnebg  3979  iinss2  4143  disjxiun  4209  trint0  4319  dtru  4390  sspwb  4413  copsexg  4442  pocl  4510  pofun  4519  solin  4526  frss  4549  tz7.7  4607  ordtri3  4617  ordtr2  4625  suc11  4685  onssneli  4691  reusv1  4723  reusv2lem1  4724  alxfr  4736  ralxfrALT  4742  iunpw  4759  ordom  4854  limom  4860  peano5  4868  2optocl  4953  3optocl  4954  ssrel  4964  ssrel2  4966  ssrelrel  4976  relop  5023  asymref2  5251  xpidtr  5256  trin2  5257  sotri3  5264  poltletr  5269  xp11  5304  relcnvtr  5389  iotaval  5429  funmo  5470  fss  5599  fv3  5744  tz6.12c  5750  tz6.12i  5751  mpteqb  5819  eldmrexrnb  5877  fornex  5970  funfvima  5973  fvclss  5980  f1veqaeq  6005  isoselem  6061  oprabid  6105  ovg  6212  bropopvvv  6426  f1o2ndf1  6454  poxp  6458  soxp  6459  mpt2xopoveqd  6472  tposfn2  6501  sorpsscmpl  6533  onnseq  6606  smoel  6622  smogt  6629  smoiso2  6631  tfrlem2  6637  tfr3  6660  tz7.48-2  6699  tz7.48-3  6701  tz7.49  6702  abianfp  6716  oecl  6781  oaordex  6801  oalimcl  6803  oaass  6804  omordi  6809  omlimcl  6821  odi  6822  omeulem1  6825  oen0  6829  oewordri  6835  nnawordi  6864  nnaass  6865  nnmordi  6874  omabs  6890  omsmolem  6896  iiner  6976  2ecoptocl  6995  3ecoptocl  6996  th3qlem2  7011  undifixp  7098  xpdom2  7203  xpf1o  7269  infensuc  7285  php  7291  onomeneq  7296  isinf  7322  findcard2  7348  unblem2  7360  infssuni  7397  finsschain  7413  marypha1  7439  hartogs  7513  card2on  7522  card2inf  7523  xpwdomg  7553  elirrv  7565  inf3lem1  7583  inf3lem2  7584  inf3lem3  7585  inf3lem5  7587  noinfep  7614  noinfepOLD  7615  trcl  7664  en3lp  7672  tcel  7684  r1sdom  7700  rankonidlem  7754  scottex  7809  pr2ne  7889  dif1card  7892  fodomnum  7938  cardaleph  7970  kmlem4  8033  kmlem9  8038  kmlem12  8041  kmlem13  8042  cflim2  8143  cfsmolem  8150  infpssrlem3  8185  isfin7-2  8276  fin1a2lem6  8285  fin1a2lem10  8289  fin1a2lem12  8291  domtriomlem  8322  axdc3lem4  8333  axdc4lem  8335  zorn2lem3  8378  zorn2lem4  8379  zorn2lem5  8380  zorn2lem6  8381  zorn2lem7  8382  zornn0g  8385  axdclem  8399  axdclem2  8400  ondomon  8438  alephval2  8447  cfpwsdom  8459  wunr1om  8594  wuncval2  8622  tskr1om  8642  grupr  8672  gruiun  8674  ingru  8690  grothomex  8704  indpi  8784  nqereu  8806  genpnnp  8882  prlem934  8910  ltaddpr2  8912  reclem2pr  8925  mulgt0sr  8980  supsrlem  8986  lemul1a  9864  squeeze0  9913  peano5nni  10003  nnunb  10217  fzind  10368  nn0ind-raph  10370  zindd  10371  eluzadd  10514  uzin  10518  xmulasslem  10864  icoshft  11019  fzen  11072  elfznelfzo  11192  injresinjlem  11199  injresinj  11200  expcllem  11392  expeq0  11410  mulexp  11419  leexp2r  11437  bernneq  11505  facdiv  11578  hasheqf1oi  11635  hashf1rn  11636  hashnn0n0nn  11664  hashle00  11669  hashgt12el  11682  hashgt12el2  11683  hash2prde  11688  hashtpg  11691  hashmap  11698  brfi1uzind  11715  cjexp  11955  absexp  12109  iseraltlem2  12476  sin01gt0  12791  alzdvds  12899  dvdslegcd  13016  gcdneg  13026  rplpwr  13056  qredeq  13106  prmpwdvds  13272  prmreclem4  13287  ramcl  13397  imasleval  13766  mreiincl  13821  mreexexd  13873  drsdirfi  14395  spwmo  14658  efgi2  15357  fiinopn  16974  tgcl  17034  distop  17060  isclo2  17152  iscldtop  17159  ssnei2  17180  opnnei  17184  pnfnei  17284  mnfnei  17285  tgcnp  17317  cnpnei  17328  bwth  17473  2ndcctbss  17518  1stcelcls  17524  txcnpi  17640  cnmptcom  17710  fbfinnfr  17873  isfildlem  17889  snfil  17896  fbunfip  17901  fgcl  17910  elfm2  17980  fmfnfmlem1  17986  fmco  17993  fbflim2  18009  flffbas  18027  cnpflf2  18032  flimfcls  18058  tmdgsum  18125  neibl  18531  metcnp3  18570  fgcfil  19224  caubl  19260  volsuplem  19449  ellimc3  19766  dvnadd  19815  dvnres  19817  cpnord  19821  dvnfre  19838  mpfrcl  19939  ply1divex  20059  aalioulem2  20250  cxpmul2  20580  wilthlem3  20853  lgsquad2lem2  21143  qabvexp  21320  uhgraeq12d  21342  ausisusgra  21380  usgraeq12d  21385  usgraedgprv  21396  usgraedgrnv  21397  usgranloop  21399  usgraedg4  21406  usgra1v  21409  usgraidx2v  21412  usgrafisinds  21427  nbgraop  21436  nbusgra  21440  nbgranself2  21448  nbgraf1olem1  21451  nbgraf1olem5  21455  nb3graprlem1  21460  cusgrarn  21468  nbcusgra  21472  cusgrasize2inds  21486  cusgrafi  21491  sizeusglecusglem1  21493  sizeusglecusg  21495  uvtxnbgra  21502  pthdepisspth  21574  spthonepeq  21587  1pthoncl  21592  2pthoncl  21603  redwlk  21606  wlkdvspth  21608  cyclnspth  21618  cyclispthon  21620  fargshiftfo  21625  usgrcyclnl1  21627  nvnencycllem  21630  3v3e3cycl1  21631  constr3trllem2  21638  4cycl4v4e  21653  4cycl4dv  21654  4cycl4dv4e  21655  vdusgraval  21678  eupatrl  21690  gxnn0add  21862  gxnn0mul  21865  ismgm  21908  isexid2  21913  zerdivemp1  22022  ipassi  22342  ubthlem2  22373  isch3  22744  shintcli  22831  shmodsi  22891  spansncvi  23154  pjjsi  23202  hoaddsub  23319  eigorthi  23340  pjss2coi  23667  pjnormssi  23671  pj3cor1i  23712  strb  23761  dmdmd  23803  mdsl0  23813  csmdsymi  23837  chrelat2i  23868  cvati  23869  mdsymlem3  23908  mdsymlem6  23911  sumdmdlem2  23922  dmdbr5ati  23925  cvmlift2lem1  24989  3ccased  25176  dedekind  25187  clim2prod  25216  prodfn0  25222  prodfrec  25223  prodmo  25262  fprodabs  25297  fprodefsum  25298  binomfallfac  25357  dfres3  25382  dfon2lem3  25412  rdgprc  25422  trpredmintr  25509  trpredrec  25516  wfr3g  25537  wfrlem12  25549  frr3g  25581  frrlem11  25594  sltval2  25611  axcontlem4  25906  cgrextend  25942  btwndiff  25961  btwnconn1lem12  26032  brsegle  26042  broutsideof2  26056  funray  26074  meran1  26161  waj-ax  26164  arg-ax  26166  wl-pm2.86i  26231  wl-exeq  26234  elicc3  26320  nn0prpwlem  26325  nn0prpw  26326  fnessref  26373  neibastop2lem  26389  filnetlem4  26410  fzmul  26444  fdc  26449  seqpo  26451  incsequz  26452  isismty  26510  ismtybndlem  26515  heibor1lem  26518  ghomco  26558  zerdivemp1x  26571  pridlc  26681  ceqsex3OLD  26709  nelss  26732  incssnn0  26765  fphpd  26877  jm2.19lem3  27062  setindtr  27095  dfac21  27141  islssfg2  27146  mpaaeu  27332  psgnunilem4  27397  stoweidlem26  27751  hirstL-ax3  27836  rexsb  27922  rexrsb  27923  2reu1  27940  afvres  28012  tz6.12-afv  28013  afvco2  28016  ndmaovdistr  28047  oprabv  28085  ssfz12  28104  elfzmlbm  28106  elfzmlbp  28107  elfzelfzelfz  28109  elfz0fzfz0  28114  fz0fzelfz0  28118  ubmelfzo  28126  ubmelm1fzo  28127  elfzonelfzo  28132  fzoopth  28139  2ffzoeq  28140  hashimarni  28164  euhash1  28167  ccatsymb  28179  swrdvalodm2  28188  swrdvalodm  28189  swrd0swrd  28197  swrdswrdlem  28198  swrdswrd  28199  swrdccatin1  28205  swrdccatin12lem3a  28208  swrdccatin12lem3b  28209  swrdccatin2  28210  swrdccatin12lem3  28212  swrdccatin12lem4  28213  swrdccatin12  28214  swrdccat3  28215  swrdccat  28216  swrdccat3blem  28218  cshwidx  28242  2cshw1lem1  28248  2cshw1lem2  28249  2cshw2lem1  28252  2cshwmod  28257  lswrdn0  28260  cshweqdif2s  28271  cshweqrep  28274  cshw1  28275  cshwsame0  28278  cshwssizelem2  28281  cshwssizelem3  28282  cshwssizelem4a  28283  cshwssizelem4  28284  cshwsexa  28291  iswlkg  28300  usg2wlkeq  28304  usgra2pthspth  28305  usgra2wlkspthlem1  28306  usgra2wlkspth  28308  usgra2pthlem1  28310  usgra2pth  28311  el2wlkonotlem  28329  el2wlkonot  28336  el2spthonot  28337  el2spthonot0  28338  el2wlkonotot0  28339  2wlkonot3v  28342  2spthonot3v  28343  usg2wotspth  28351  2pthwlkonot  28352  2spontn0vne  28354  usg2spthonot  28355  usg2spthonot0  28356  rusgrargra  28373  frgraunss  28385  frgra2v  28389  frgra3vlem1  28390  frgra3vlem2  28391  3vfriswmgralem  28394  3vfriswmgra  28395  2pthfrgra  28401  3cyclfrgrarn1  28402  n4cyclfrgra  28408  frgranbnb  28410  vdn0frgrav2  28414  vdgn0frgrav2  28415  frgrancvvdeqlem2  28420  frgrancvvdeqlem3  28421  frgrancvvdeqlem4  28422  frgrancvvdeqlem7  28425  frgrancvvdeqlemA  28426  frgrancvvdeqlemB  28427  frgrancvvdeqlemC  28428  frgrawopreglem3  28435  frgrawopreglem4  28436  frgrawopreglem5  28437  frgrawopreg  28438  frgrawopreg1  28439  frgrawopreg2  28440  frg2wot1  28446  frg2woteqm  28448  frg2woteq  28449  2spotdisj  28450  usg2spot2nb  28454  usgreg2spot  28456  2spotmdisj  28457  frgregordn0  28459  sb5ALT  28609  truniALT  28626  onfrALTlem3  28630  ee223  28735  3orbi123VD  28962  sbc3orgVD  28963  exbirVD  28965  exbiriVD  28966  sbcim2gVD  28987  trsbcVD  28989  truniALTVD  28990  onfrALTlem3VD  28999  onfrALTlem2VD  29001  csbrngVD  29008  19.41rgVD  29014  a9e2eqVD  29019  a9e2ndeqVD  29021  2uasbanhVD  29023  sb5ALTVD  29025  vk15.4jVD  29026  ax12olem3aAUX7  29457  ax10lem4NEW7  29471  sb6rfNEW7  29592  sb56NEW7  29596  exsbNEW7  29599  ax11bNEW7  29622  cdleme18d  31092  tendovalco  31562  cdlemn11pre  32008  dihord2pre  32023
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator