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  sbequ2OLD  1658  equtrr  1691  ax12olem3OLD  1979  ax10lem2  1989  ax10lem4OLD  1996  equveli  2042  ax11b  2048  sb6rf  2140  sb56  2147  exsb  2180  mo  2276  exmoeu  2296  morimv  2302  eupickbi  2320  2mo  2332  2eu1  2334  exists2  2344  r19.12  2779  2gencl  2945  3gencl  2946  rspccv  3009  ceqex  3026  mob  3076  euind  3081  reuind  3097  2rmorex  3098  sseq2  3330  reupick2  3587  uneqdifeq  3676  difsn  3893  eqsn  3920  preq12b  3934  prnebg  3939  iinss2  4103  disjxiun  4169  trint0  4279  dtru  4350  sspwb  4373  copsexg  4402  pocl  4470  pofun  4479  solin  4486  frss  4509  tz7.7  4567  ordtri3  4577  ordtr2  4585  suc11  4644  onssneli  4650  reusv1  4682  reusv2lem1  4683  alxfr  4695  ralxfrALT  4701  iunpw  4718  ordom  4813  limom  4819  peano5  4827  2optocl  4912  3optocl  4913  ssrel  4923  ssrel2  4925  ssrelrel  4935  relop  4982  asymref2  5210  xpidtr  5215  trin2  5216  sotri3  5223  poltletr  5228  xp11  5263  relcnvtr  5348  iotaval  5388  funmo  5429  fss  5558  fv3  5703  tz6.12c  5709  tz6.12i  5710  mpteqb  5778  eldmrexrnb  5836  fornex  5929  funfvima  5932  fvclss  5939  f1veqaeq  5964  isoselem  6020  oprabid  6064  ovg  6171  bropopvvv  6385  f1o2ndf1  6413  poxp  6417  soxp  6418  mpt2xopoveqd  6431  tposfn2  6460  sorpsscmpl  6492  onnseq  6565  smoel  6581  smogt  6588  smoiso2  6590  tfrlem2  6596  tfr3  6619  tz7.48-2  6658  tz7.48-3  6660  tz7.49  6661  abianfp  6675  oecl  6740  oaordex  6760  oalimcl  6762  oaass  6763  omordi  6768  omlimcl  6780  odi  6781  omeulem1  6784  oen0  6788  oewordri  6794  nnawordi  6823  nnaass  6824  nnmordi  6833  omabs  6849  omsmolem  6855  iiner  6935  2ecoptocl  6954  3ecoptocl  6955  th3qlem2  6970  undifixp  7057  xpdom2  7162  xpf1o  7228  infensuc  7244  php  7250  onomeneq  7255  isinf  7281  findcard2  7307  unblem2  7319  finsschain  7371  marypha1  7397  hartogs  7469  card2on  7478  card2inf  7479  xpwdomg  7509  elirrv  7521  inf3lem1  7539  inf3lem2  7540  inf3lem3  7541  inf3lem5  7543  noinfep  7570  noinfepOLD  7571  trcl  7620  en3lp  7628  tcel  7640  r1sdom  7656  rankonidlem  7710  scottex  7765  pr2ne  7845  dif1card  7848  fodomnum  7894  cardaleph  7926  kmlem4  7989  kmlem9  7994  kmlem12  7997  kmlem13  7998  cflim2  8099  cfsmolem  8106  infpssrlem3  8141  isfin7-2  8232  fin1a2lem6  8241  fin1a2lem10  8245  fin1a2lem12  8247  domtriomlem  8278  axdc3lem4  8289  axdc4lem  8291  zorn2lem3  8334  zorn2lem4  8335  zorn2lem5  8336  zorn2lem6  8337  zorn2lem7  8338  zornn0g  8341  axdclem  8355  axdclem2  8356  ondomon  8394  alephval2  8403  cfpwsdom  8415  wunr1om  8550  wuncval2  8578  tskr1om  8598  grupr  8628  gruiun  8630  ingru  8646  grothomex  8660  indpi  8740  nqereu  8762  genpnnp  8838  prlem934  8866  ltaddpr2  8868  reclem2pr  8881  mulgt0sr  8936  supsrlem  8942  lemul1a  9820  squeeze0  9869  peano5nni  9959  nnunb  10173  fzind  10324  nn0ind-raph  10326  zindd  10327  eluzadd  10470  uzin  10474  xmulasslem  10820  icoshft  10975  fzen  11028  elfznelfzo  11147  injresinjlem  11154  injresinj  11155  expcllem  11347  expeq0  11365  mulexp  11374  leexp2r  11392  bernneq  11460  facdiv  11533  hasheqf1oi  11590  hashf1rn  11591  hashnn0n0nn  11619  hashle00  11624  hashgt12el  11637  hashgt12el2  11638  hash2prde  11643  hashtpg  11646  hashmap  11653  brfi1uzind  11670  cjexp  11910  absexp  12064  iseraltlem2  12431  sin01gt0  12746  alzdvds  12854  dvdslegcd  12971  gcdneg  12981  rplpwr  13011  qredeq  13061  prmpwdvds  13227  prmreclem4  13242  ramcl  13352  imasleval  13721  mreiincl  13776  mreexexd  13828  drsdirfi  14350  spwmo  14613  efgi2  15312  fiinopn  16929  tgcl  16989  distop  17015  isclo2  17107  iscldtop  17114  ssnei2  17135  opnnei  17139  pnfnei  17238  mnfnei  17239  tgcnp  17271  cnpnei  17282  2ndcctbss  17471  1stcelcls  17477  txcnpi  17593  cnmptcom  17663  fbfinnfr  17826  isfildlem  17842  snfil  17849  fbunfip  17854  fgcl  17863  elfm2  17933  fmfnfmlem1  17939  fmco  17946  fbflim2  17962  flffbas  17980  cnpflf2  17985  flimfcls  18011  tmdgsum  18078  neibl  18484  metcnp3  18523  fgcfil  19177  caubl  19213  volsuplem  19402  ellimc3  19719  dvnadd  19768  dvnres  19770  cpnord  19774  dvnfre  19791  mpfrcl  19892  ply1divex  20012  aalioulem2  20203  cxpmul2  20533  wilthlem3  20806  lgsquad2lem2  21096  qabvexp  21273  uhgraeq12d  21295  ausisusgra  21333  usgraeq12d  21338  usgraedgprv  21349  usgraedgrnv  21350  usgranloop  21352  usgraedg4  21359  usgra1v  21362  usgraidx2v  21365  usgrafisinds  21380  nbgraop  21389  nbusgra  21393  nbgranself2  21401  nbgraf1olem1  21404  nbgraf1olem5  21408  nb3graprlem1  21413  cusgrarn  21421  nbcusgra  21425  cusgrasize2inds  21439  cusgrafi  21444  sizeusglecusglem1  21446  sizeusglecusg  21448  uvtxnbgra  21455  pthdepisspth  21527  spthonepeq  21540  1pthoncl  21545  2pthoncl  21556  redwlk  21559  wlkdvspth  21561  cyclnspth  21571  cyclispthon  21573  fargshiftfo  21578  usgrcyclnl1  21580  nvnencycllem  21583  3v3e3cycl1  21584  constr3trllem2  21591  4cycl4v4e  21606  4cycl4dv  21607  4cycl4dv4e  21608  vdusgraval  21631  eupatrl  21643  gxnn0add  21815  gxnn0mul  21818  ismgm  21861  isexid2  21866  zerdivemp1  21975  ipassi  22295  ubthlem2  22326  isch3  22697  shintcli  22784  shmodsi  22844  spansncvi  23107  pjjsi  23155  hoaddsub  23272  eigorthi  23293  pjss2coi  23620  pjnormssi  23624  pj3cor1i  23665  strb  23714  dmdmd  23756  mdsl0  23766  csmdsymi  23790  chrelat2i  23821  cvati  23822  mdsymlem3  23861  mdsymlem6  23864  sumdmdlem2  23875  dmdbr5ati  23878  cvmlift2lem1  24942  3ccased  25129  dedekind  25140  clim2prod  25169  prodfn0  25175  prodfrec  25176  prodmo  25215  fprodabs  25250  fprodefsum  25251  binomfallfac  25308  dfres3  25330  dfon2lem3  25355  rdgprc  25365  trpredmintr  25448  trpredrec  25455  wfr3g  25469  wfrlem12  25481  frr3g  25494  frrlem11  25507  sltval2  25524  axcontlem4  25810  cgrextend  25846  btwndiff  25865  btwnconn1lem12  25936  brsegle  25946  broutsideof2  25960  funray  25978  meran1  26065  waj-ax  26068  arg-ax  26070  wl-pm2.86i  26135  elicc3  26210  nn0prpwlem  26215  nn0prpw  26216  fnessref  26263  neibastop2lem  26279  filnetlem4  26300  fzmul  26334  fdc  26339  seqpo  26341  incsequz  26342  isismty  26400  ismtybndlem  26405  heibor1lem  26408  ghomco  26448  zerdivemp1x  26461  pridlc  26571  ceqsex3OLD  26599  nelss  26622  incssnn0  26655  fphpd  26767  jm2.19lem3  26952  setindtr  26985  dfac21  27032  islssfg2  27037  mpaaeu  27223  psgnunilem4  27288  stoweidlem26  27642  hirstL-ax3  27727  rexsb  27813  rexrsb  27814  2reu1  27831  afvres  27903  tz6.12-afv  27904  afvco2  27907  ndmaovdistr  27938  ssfz12  27976  elfzmlbm  27977  elfzmlbp  27978  elfzelfzelfz  27981  ubmelfzo  27986  ubmelm1fzo  27987  elfzonelfzo  27992  hashimarni  27995  euhash1  27998  swrd0swrd  28009  swrdswrdlem  28010  swrdswrd  28011  swrdccatin1  28016  swrdccatin2  28018  swrdccatin12lem3a  28021  swrdccatin12lem3b  28022  swrdccatin12lem3c  28023  swrdccatin12lem3  28024  swrdccatin12lem4  28025  swrdccatin12  28026  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3  28029  swrdccat3b  28031  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspth  28038  usgra2pthlem1  28040  usgra2pth  28041  el2wlkonotlem  28059  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  el2wlkonotot0  28069  2wlkonot3v  28072  2spthonot3v  28073  usg2wotspth  28081  2pthwlkonot  28082  2spontn0vne  28084  usg2spthonot  28085  usg2spthonot0  28086  frgraunss  28099  frgra2v  28103  frgra3vlem1  28104  frgra3vlem2  28105  3vfriswmgralem  28108  3vfriswmgra  28109  2pthfrgra  28115  3cyclfrgrarn1  28116  n4cyclfrgra  28122  frgranbnb  28124  vdn0frgrav2  28128  vdgn0frgrav2  28129  frgrancvvdeqlem2  28134  frgrancvvdeqlem3  28135  frgrancvvdeqlem4  28136  frgrancvvdeqlem7  28139  frgrancvvdeqlemA  28140  frgrancvvdeqlemB  28141  frgrancvvdeqlemC  28142  frgrawopreglem3  28149  frgrawopreglem4  28150  frgrawopreglem5  28151  frgrawopreg  28152  frgrawopreg1  28153  frgrawopreg2  28154  frg2wot1  28160  frg2woteqm  28162  frg2woteq  28163  2spotdisj  28164  usg2spot2nb  28168  usgreg2spot  28170  2spotmdisj  28171  frgregordn0  28173  sb5ALT  28320  truniALT  28337  onfrALTlem3  28341  ee223  28444  3orbi123VD  28671  sbc3orgVD  28672  exbirVD  28674  exbiriVD  28675  sbcim2gVD  28696  trsbcVD  28698  truniALTVD  28699  onfrALTlem3VD  28708  onfrALTlem2VD  28710  csbrngVD  28717  19.41rgVD  28723  a9e2eqVD  28728  a9e2ndeqVD  28730  2uasbanhVD  28732  sb5ALTVD  28734  vk15.4jVD  28735  ax12olem3aAUX7  29163  ax10lem4NEW7  29177  sb6rfNEW7  29293  sb56NEW7  29297  exsbNEW7  29300  ax11bNEW7  29323  cdleme18d  30777  tendovalco  31247  cdlemn11pre  31693  dihord2pre  31708
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator