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  1383  meredith  1413  sbequ2  1660  sbequ2OLD  1661  equtrr  1695  cbv1  1973  ax12olem3OLD  2013  ax10lem2  2023  ax10lem4OLD  2030  dvelimdf  2066  ax11b  2078  equveli  2081  sbied  2123  sbequi  2136  sb6rf  2166  sb56  2173  exsb  2206  mo  2302  exmoeu  2322  morimv  2328  eupickbi  2346  2mo  2358  2eu1  2360  exists2  2370  r19.12  2811  2gencl  2977  3gencl  2978  rspccv  3041  ceqex  3058  mob  3108  euind  3113  reuind  3129  2rmorex  3130  sseq2  3362  reupick2  3619  uneqdifeq  3708  difsn  3925  eqsn  3952  preq12b  3966  prnebg  3971  iinss2  4135  disjxiun  4201  trint0  4311  dtru  4382  sspwb  4405  copsexg  4434  pocl  4502  pofun  4511  solin  4518  frss  4541  tz7.7  4599  ordtri3  4609  ordtr2  4617  suc11  4676  onssneli  4682  reusv1  4714  reusv2lem1  4715  alxfr  4727  ralxfrALT  4733  iunpw  4750  ordom  4845  limom  4851  peano5  4859  2optocl  4944  3optocl  4945  ssrel  4955  ssrel2  4957  ssrelrel  4967  relop  5014  asymref2  5242  xpidtr  5247  trin2  5248  sotri3  5255  poltletr  5260  xp11  5295  relcnvtr  5380  iotaval  5420  funmo  5461  fss  5590  fv3  5735  tz6.12c  5741  tz6.12i  5742  mpteqb  5810  eldmrexrnb  5868  fornex  5961  funfvima  5964  fvclss  5971  f1veqaeq  5996  isoselem  6052  oprabid  6096  ovg  6203  bropopvvv  6417  f1o2ndf1  6445  poxp  6449  soxp  6450  mpt2xopoveqd  6463  tposfn2  6492  sorpsscmpl  6524  onnseq  6597  smoel  6613  smogt  6620  smoiso2  6622  tfrlem2  6628  tfr3  6651  tz7.48-2  6690  tz7.48-3  6692  tz7.49  6693  abianfp  6707  oecl  6772  oaordex  6792  oalimcl  6794  oaass  6795  omordi  6800  omlimcl  6812  odi  6813  omeulem1  6816  oen0  6820  oewordri  6826  nnawordi  6855  nnaass  6856  nnmordi  6865  omabs  6881  omsmolem  6887  iiner  6967  2ecoptocl  6986  3ecoptocl  6987  th3qlem2  7002  undifixp  7089  xpdom2  7194  xpf1o  7260  infensuc  7276  php  7282  onomeneq  7287  isinf  7313  findcard2  7339  unblem2  7351  infssuni  7388  finsschain  7404  marypha1  7430  hartogs  7502  card2on  7511  card2inf  7512  xpwdomg  7542  elirrv  7554  inf3lem1  7572  inf3lem2  7573  inf3lem3  7574  inf3lem5  7576  noinfep  7603  noinfepOLD  7604  trcl  7653  en3lp  7661  tcel  7673  r1sdom  7689  rankonidlem  7743  scottex  7798  pr2ne  7878  dif1card  7881  fodomnum  7927  cardaleph  7959  kmlem4  8022  kmlem9  8027  kmlem12  8030  kmlem13  8031  cflim2  8132  cfsmolem  8139  infpssrlem3  8174  isfin7-2  8265  fin1a2lem6  8274  fin1a2lem10  8278  fin1a2lem12  8280  domtriomlem  8311  axdc3lem4  8322  axdc4lem  8324  zorn2lem3  8367  zorn2lem4  8368  zorn2lem5  8369  zorn2lem6  8370  zorn2lem7  8371  zornn0g  8374  axdclem  8388  axdclem2  8389  ondomon  8427  alephval2  8436  cfpwsdom  8448  wunr1om  8583  wuncval2  8611  tskr1om  8631  grupr  8661  gruiun  8663  ingru  8679  grothomex  8693  indpi  8773  nqereu  8795  genpnnp  8871  prlem934  8899  ltaddpr2  8901  reclem2pr  8914  mulgt0sr  8969  supsrlem  8975  lemul1a  9853  squeeze0  9902  peano5nni  9992  nnunb  10206  fzind  10357  nn0ind-raph  10359  zindd  10360  eluzadd  10503  uzin  10507  xmulasslem  10853  icoshft  11008  fzen  11061  elfznelfzo  11180  injresinjlem  11187  injresinj  11188  expcllem  11380  expeq0  11398  mulexp  11407  leexp2r  11425  bernneq  11493  facdiv  11566  hasheqf1oi  11623  hashf1rn  11624  hashnn0n0nn  11652  hashle00  11657  hashgt12el  11670  hashgt12el2  11671  hash2prde  11676  hashtpg  11679  hashmap  11686  brfi1uzind  11703  cjexp  11943  absexp  12097  iseraltlem2  12464  sin01gt0  12779  alzdvds  12887  dvdslegcd  13004  gcdneg  13014  rplpwr  13044  qredeq  13094  prmpwdvds  13260  prmreclem4  13275  ramcl  13385  imasleval  13754  mreiincl  13809  mreexexd  13861  drsdirfi  14383  spwmo  14646  efgi2  15345  fiinopn  16962  tgcl  17022  distop  17048  isclo2  17140  iscldtop  17147  ssnei2  17168  opnnei  17172  pnfnei  17272  mnfnei  17273  tgcnp  17305  cnpnei  17316  bwth  17461  2ndcctbss  17506  1stcelcls  17512  txcnpi  17628  cnmptcom  17698  fbfinnfr  17861  isfildlem  17877  snfil  17884  fbunfip  17889  fgcl  17898  elfm2  17968  fmfnfmlem1  17974  fmco  17981  fbflim2  17997  flffbas  18015  cnpflf2  18020  flimfcls  18046  tmdgsum  18113  neibl  18519  metcnp3  18558  fgcfil  19212  caubl  19248  volsuplem  19437  ellimc3  19754  dvnadd  19803  dvnres  19805  cpnord  19809  dvnfre  19826  mpfrcl  19927  ply1divex  20047  aalioulem2  20238  cxpmul2  20568  wilthlem3  20841  lgsquad2lem2  21131  qabvexp  21308  uhgraeq12d  21330  ausisusgra  21368  usgraeq12d  21373  usgraedgprv  21384  usgraedgrnv  21385  usgranloop  21387  usgraedg4  21394  usgra1v  21397  usgraidx2v  21400  usgrafisinds  21415  nbgraop  21424  nbusgra  21428  nbgranself2  21436  nbgraf1olem1  21439  nbgraf1olem5  21443  nb3graprlem1  21448  cusgrarn  21456  nbcusgra  21460  cusgrasize2inds  21474  cusgrafi  21479  sizeusglecusglem1  21481  sizeusglecusg  21483  uvtxnbgra  21490  pthdepisspth  21562  spthonepeq  21575  1pthoncl  21580  2pthoncl  21591  redwlk  21594  wlkdvspth  21596  cyclnspth  21606  cyclispthon  21608  fargshiftfo  21613  usgrcyclnl1  21615  nvnencycllem  21618  3v3e3cycl1  21619  constr3trllem2  21626  4cycl4v4e  21641  4cycl4dv  21642  4cycl4dv4e  21643  vdusgraval  21666  eupatrl  21678  gxnn0add  21850  gxnn0mul  21853  ismgm  21896  isexid2  21901  zerdivemp1  22010  ipassi  22330  ubthlem2  22361  isch3  22732  shintcli  22819  shmodsi  22879  spansncvi  23142  pjjsi  23190  hoaddsub  23307  eigorthi  23328  pjss2coi  23655  pjnormssi  23659  pj3cor1i  23700  strb  23749  dmdmd  23791  mdsl0  23801  csmdsymi  23825  chrelat2i  23856  cvati  23857  mdsymlem3  23896  mdsymlem6  23899  sumdmdlem2  23910  dmdbr5ati  23913  cvmlift2lem1  24977  3ccased  25164  dedekind  25175  clim2prod  25205  prodfn0  25211  prodfrec  25212  prodmo  25251  fprodabs  25286  fprodefsum  25287  binomfallfac  25346  dfres3  25371  dfon2lem3  25396  rdgprc  25406  trpredmintr  25489  trpredrec  25496  wfr3g  25510  wfrlem12  25522  frr3g  25535  frrlem11  25548  sltval2  25565  axcontlem4  25854  cgrextend  25890  btwndiff  25909  btwnconn1lem12  25980  brsegle  25990  broutsideof2  26004  funray  26022  meran1  26109  waj-ax  26112  arg-ax  26114  wl-pm2.86i  26179  wl-exeq  26182  elicc3  26257  nn0prpwlem  26262  nn0prpw  26263  fnessref  26310  neibastop2lem  26326  filnetlem4  26347  fzmul  26381  fdc  26386  seqpo  26388  incsequz  26389  isismty  26447  ismtybndlem  26452  heibor1lem  26455  ghomco  26495  zerdivemp1x  26508  pridlc  26618  ceqsex3OLD  26646  nelss  26669  incssnn0  26702  fphpd  26814  jm2.19lem3  26999  setindtr  27032  dfac21  27079  islssfg2  27084  mpaaeu  27270  psgnunilem4  27335  stoweidlem26  27689  hirstL-ax3  27774  rexsb  27860  rexrsb  27861  2reu1  27878  afvres  27950  tz6.12-afv  27951  afvco2  27954  ndmaovdistr  27985  ssfz12  28026  elfzmlbm  28027  elfzmlbp  28028  elfzelfzelfz  28031  ubmelfzo  28038  ubmelm1fzo  28039  elfzonelfzo  28044  hashimarni  28068  euhash1  28071  swrd0swrd  28084  swrdswrdlem  28085  swrdswrd  28086  swrdccatin1  28091  swrdccatin2  28093  swrdccatin12lem3a  28096  swrdccatin12lem3b  28097  swrdccatin12lem3c  28098  swrdccatin12lem3  28099  swrdccatin12lem4  28100  swrdccatin12  28101  swrdccatin12b  28102  swrdccatin12c  28103  swrdccat3  28104  swrdccat3b  28106  shwrdidx  28130  shwrdidxmod  28131  2shwrd1lem1  28136  2shwrd1lem2  28137  2shwrd1lem3  28138  2shwrd2lem1  28142  lswrdn0  28149  shwrdeqdif2lem2  28155  shwrdeqdif2  28156  shwrdeqdif2s  28157  shwrdeqrep  28160  shwrd1  28161  shwrdsame0  28164  shwrdssizelem2  28167  shwrdssizelem3  28168  shwrdssizelem4a  28169  shwrdssizelem4  28170  usgra2pthspth  28179  usgra2wlkspthlem1  28180  usgra2wlkspth  28182  usgra2pthlem1  28184  usgra2pth  28185  el2wlkonotlem  28203  el2wlkonot  28210  el2spthonot  28211  el2spthonot0  28212  el2wlkonotot0  28213  2wlkonot3v  28216  2spthonot3v  28217  usg2wotspth  28225  2pthwlkonot  28226  2spontn0vne  28228  usg2spthonot  28229  usg2spthonot0  28230  frgraunss  28243  frgra2v  28247  frgra3vlem1  28248  frgra3vlem2  28249  3vfriswmgralem  28252  3vfriswmgra  28253  2pthfrgra  28259  3cyclfrgrarn1  28260  n4cyclfrgra  28266  frgranbnb  28268  vdn0frgrav2  28272  vdgn0frgrav2  28273  frgrancvvdeqlem2  28278  frgrancvvdeqlem3  28279  frgrancvvdeqlem4  28280  frgrancvvdeqlem7  28283  frgrancvvdeqlemA  28284  frgrancvvdeqlemB  28285  frgrancvvdeqlemC  28286  frgrawopreglem3  28293  frgrawopreglem4  28294  frgrawopreglem5  28295  frgrawopreg  28296  frgrawopreg1  28297  frgrawopreg2  28298  frg2wot1  28304  frg2woteqm  28306  frg2woteq  28307  2spotdisj  28308  usg2spot2nb  28312  usgreg2spot  28314  2spotmdisj  28315  frgregordn0  28317  sb5ALT  28464  truniALT  28481  onfrALTlem3  28485  ee223  28589  3orbi123VD  28816  sbc3orgVD  28817  exbirVD  28819  exbiriVD  28820  sbcim2gVD  28841  trsbcVD  28843  truniALTVD  28844  onfrALTlem3VD  28853  onfrALTlem2VD  28855  csbrngVD  28862  19.41rgVD  28868  a9e2eqVD  28873  a9e2ndeqVD  28875  2uasbanhVD  28877  sb5ALTVD  28879  vk15.4jVD  28880  ax12olem3aAUX7  29311  ax10lem4NEW7  29325  sb6rfNEW7  29441  sb56NEW7  29445  exsbNEW7  29448  ax11bNEW7  29471  cdleme18d  30931  tendovalco  31401  cdlemn11pre  31847  dihord2pre  31862
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator