HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
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  1553  ax12olem23  1555  ax10lem16  1563  ax10  1575  hbimd  1668  19.21t  1671  equtrr  1689  sbequ2  1743  ax11b  1789  sb6rf  1831  sb56  1837  exmoeu  1991  moimv  1997  eupickbi  2015  2eu1  2029  exists2  2039  r19.12  2378  2gencl  2503  3gencl  2504  rcla4cv  2558  ceqex  2573  mob  2630  euind  2635  reuind  2649  sseq2  2836  uneqdifeq  3158  difsn  3363  eqsn  3379  preq12b  3390  intab  3488  iinss2  3549  trint0  3690  dtru  3758  sspwb  3778  copsexg  3806  pocl  3872  pofun  3881  solin  3888  frss  3911  tz7.7  3969  ordtri3  3979  ordtr2  3987  suc11  4045  onssneli  4051  eusv2  4095  ralxfrALT  4119  iunpw  4137  ordom  4232  limom  4238  peano5  4246  2optocl  4348  3optocl  4349  ssrel  4359  ssrelrel  4369  relop  4416  xpidtr  4646  trin2  4647  sotri3  4654  poltletr  4659  xp11  4692  relcnvtr  4772  funmo  4801  fss  4925  fv3  5060  tz6.12-1  5063  tz6.12c  5067  tz6.12i  5068  mpteqb  5130  fornex  5199  funfvima  5265  fvclss  5272  f1fveq  5297  isotr  5337  isotrALT  5338  isoselem  5343  oprabid  5384  ovg  5481  poxp  5712  soxp  5713  tposfn2  5739  sorpsscmpl  5767  iotaval  5781  onnseq  5816  smores  5824  smoel  5832  smogt  5839  smoiso2  5841  tfrlem2  5847  tfr3  5870  tz7.48-2  5909  tz7.48-3  5911  tz7.49  5912  abianfp  5926  oecl  5991  oaordex  6011  oalimcl  6013  oaass  6014  omordi  6019  omlimcl  6031  odi  6032  omeulem1  6035  oen0  6039  oewordri  6045  nnawordi  6074  nnaass  6075  nnmordi  6084  omabs  6100  omsmolem  6106  iiner  6186  2ecoptocl  6194  3ecoptocl  6195  th3qlem2  6210  undifixp  6290  xpdom2  6394  xpf1o  6507  infensuc  6523  php  6529  onomeneq  6534  isinf  6559  findcard2  6581  unblem2  6593  finsschain  6644  marypha1  6669  supub  6690  suplub  6691  supsnALT  6706  hartogs  6742  card2on  6751  card2inf  6752  xpwdomg  6782  elirrv  6794  inf3lem1  6812  inf3lem2  6813  inf3lem3  6814  inf3lem5  6816  noinfep  6843  noinfepOLD  6844  trcl  6893  en3lp  6901  tcel  6913  r1sdom  6929  rankonidlem  6982  rankxpsuc  7034  scottex  7037  pr2ne  7117  dif1card  7120  fodomnum  7166  cardaleph  7198  cflim2  7352  cfsmolem  7359  infpssrlem3  7394  isfin7-2  7485  fin1a2lem6  7494  fin1a2lem10  7498  fin1a2lem12  7500  domtriomlem  7531  axdc3lem4  7542  axdc4lem  7544  kmlem4  7582  kmlem9  7587  kmlem12  7590  kmlem13  7591  zorn2lem3  7601  zorn2lem4  7602  zorn2lem5  7603  zorn2lem6  7604  zorn2lem7  7605  zornn0g  7608  axdclem  7622  axdclem2  7623  ondomon  7659  alephval2  7666  cfpwsdom  7678  axrepnd  7688  tskr1om  7813  grupr  7841  gruiun  7843  ingru  7858  grothomex  7872  indpi  7952  nqereu  7974  genpnnp  8050  prlem934  8078  ltaddpr2  8080  reclem2pr  8093  mulgt0sr  8148  supsrlem  8154  lemul1a  8989  squeeze0  9038  peano5nni  9127  nnunb  9330  fzind  9478  nn0ind-raph  9481  zindd  9482  eluzadd  9625  uzin  9629  xmulasslem  9973  icoshft  10123  fzen  10174  expcllem  10469  expeq0  10487  mulexp  10496  leexp2r  10514  bernneq  10581  facdiv  10654  hashmap  10740  cjexp  10830  absexp  10981  iseraltlem2  11346  sin01gt0  11653  alzdvds  11760  dvdslegcd  11800  gcdneg  11810  rplpwr  11840  qredeq  11890  prmpwdvds  12056  prmreclem4  12071  ramcl  12181  imasleval  12527  mreiincl  12580  drsdirfi  12632  spwmo  12886  efgi2  13743  fiinopn  15353  tgcl  15413  distop  15439  isclo2  15530  iscldtop  15537  ssnei2  15558  opnnei  15562  pnfnei  15641  mnfnei  15642  tgcnp  15674  cnpnei  15684  2ndcctbss  15868  1stcelcls  15874  txcnpi  15989  cnmptcom  16059  fbfinnfr  16223  isfildlem  16239  snfil  16246  fbunfip  16251  fgcl  16260  elfm2  16330  fmfnfmlem1  16336  fmco  16343  fbflim2  16359  flffbas  16377  cnpflf2  16382  flimfcls  16408  tmdgsum  16465  xmeteq0  16590  neibl  16735  metcnp3  16774  fgcfil  17377  caubl  17413  volsuplem  17592  dvnadd  17934  dvnres  17935  cpnord  17939  mpfrcl  18047  ply1divex  18165  cxpmul2  18626  wilthlem3  18862  lgsquad2lem2  19152  qabvexp  19329  gxnn0add  19474  gxnn0mul  19477  ismgm  19520  isexid2  19525  rngodm1dm2  19618  ipassi  19952  ubthlem2  19983  isch3  20354  shintcli  20441  shmodsi  20501  spansncvi  20782  pjjsi  20830  hoaddsub  20929  eigorthi  20950  pjss2coi  21277  pjnormssi  21281  pj3cor1i  21322  strb  21371  dmdmd  21413  mdsl0  21423  csmdsymi  21447  chrelat2i  21478  cvati  21479  mdsymlem3  21518  mdsymlem6  21521  sumdmdlem2  21532  dmdbr5ati  21535  cvmlift2lem1  21707  3ccased  21952  dedekind  21956  dfres3  21988  dfon2lem3  22011  rdgprc  22021  trpredmintr  22105  trpredrec  22112  wfr3g  22126  wfrlem12  22138  frr3g  22151  frrlem11  22164  sltval2  22180  axfelem13  22229  elfuns  22331  axcontlem4  22472  cgrextend  22508  btwndiff  22527  btwnconn1lem12  22598  brsegle  22608  broutsideof2  22622  funray  22640  meran1  22702  waj-ax  22705  arg-ax  22707  wl-pm2.86i  22773  copsexgb  22808  evpexun  22837  isunscov  22889  restidsing  22891  twsymr  22893  prj1b  22894  prj3  22895  fixpc  22909  domintrefc  22941  mapmapmap  22965  injsurinj  22966  repfuntw  22977  cbcpcp  22979  prl  22984  prl2  22986  prjmapcp2  22987  dstr  22988  jidd  23009  midd  23010  int2pre  23054  ubpar  23078  inposet  23095  tolat  23103  toplat  23107  latdir  23112  ridlideq  23152  rzrlzreq  23153  resgcom  23168  grpodivone  23190  grpodivfo  23191  rltrran  23231  zerdivemp1  23253  zintdom  23255  muldisc  23301  svli2  23304  svs2  23307  truni1  23325  truni2  23326  truni3  23327  inttop2  23338  npmp  23344  nsn  23353  intopcoaconlem3b  23361  intopcoaconc  23364  qusp  23365  intcont  23366  prcnt  23374  fisub  23377  cmptdst  23391  exopcopn  23395  prdnei  23396  limptlimpr2lem1  23397  limptlimpr2lem2  23398  islimrs  23403  islimrs3  23404  islimrs4  23405  bwt2  23415  iintlem1  23433  iint  23435  lvsovso  23449  supnuf  23452  claddrvr  23471  sigadd  23472  addcomv  23478  addcanrg  23490  negveudr  23492  subclrvd  23497  distsava  23512  intvconlem1  23526  hdrmp  23529  cmppfd  23568  domcmpd  23569  codcmpd  23570  cmpasso  23596  cmpida  23597  cmpidb  23598  cmpassoh  23624  homgrf  23625  imonclem  23636  cmpmon  23638  iepiclem  23646  isepic  23647  idfisf  23664  issrc  23690  propsrc  23691  partarelt1  23719  inttaror  23723  inttarcar  23724  fnctartar  23730  fnctartar2  23731  prismorcset2  23741  cmpmor  23798  setiscat  23802  lemindclsbu  23816  indcls2  23817  clscnc  23831  pgapspf2  23874  lineval5a  23904  lineval6a  23905  isconcl5a  23918  isconcl6a  23919  isibg1a1  23928  isibg1a2  23929  isibg2a  23930  isibg1a3a  23931  isibg1a4a  23932  isibg1a5a  23933  sgplpte21d  23943  elicc3  24002  nn0prpwlem  24012  nn0prpw  24013  fnessref  24067  neibastop2lem  24083  filnetlem4  24104  fzmul  24218  fdc  24230  seqpo  24232  incsequz  24233  isismty  24300  ismtybndlem  24305  heibor1lem  24308  ghomco  24348  zerdivemp1x  24361  pridlc  24471  ceqsex3OLD  24501  nelss  24526  incssnn0  24563  fphpd  24673  jm2.19lem3  24858  setindtr  24891  dfac21  24942  aalioulem2  24956  islssfg2  24986  mpaaeu  25172  psgnunilem4  25237  pm14.24  25453  hirstL-ax3  25506  sb5ALT  25596  truniALT  25613  onfrALTlem3  25617  ee223  25706  3orbi123VD  25869  sbc3orgVD  25870  exbirVD  25872  exbiriVD  25873  sbcim2gVD  25894  trsbcVD  25896  truniALTVD  25897  onfrALTlem3VD  25906  onfrALTlem2VD  25908  csbrngVD  25915  19.41rgVD  25921  a9e2eqVD  25926  a9e2ndeqVD  25928  2uasbanhVD  25930  sb5ALTVD  25932  vk15.4jVD  25933  ax12-3  27453  ax9lem2  27490  ax9lem5  27493  ax9lem15  27503  ax9vax9  27507  cdleme18d  28833  tendovalco  29303  cdlemn11pre  29749  dihord2pre  29764
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain