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 21 . 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 6
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  213  syl5ibrcom  215  pm5.501  332  jaod  371  orel1  373  pm2.62  400  impcom  421  imp3a  422  expcom  426  exp3a  427  pm3.21  437  imdistanri  675  pm2.64  767  pm2.75  825  ccased  918  dedlem0b  924  3impd  1170  3expd  1173  mp3an1i  1275  simplbi2com  1370  meredith  1400  ax12olem21  1655  ax12olem23  1657  ax10lem16  1665  ax10lem26  1675  ax10  1677  hbimd  1809  equtrr  1827  sbequ2  1891  ax11b  1943  sb6rf  1986  sb56  1992  mo  2138  exmoeu  2158  moimv  2164  eupickbi  2182  2mo  2194  2eu1  2196  exists2  2206  r19.12  2627  2gencl  2768  3gencl  2769  rcla4cv  2832  ceqex  2849  mob  2898  euind  2903  reuind  2917  sseq2  3142  reupick2  3396  uneqdifeq  3484  difsn  3696  eqsn  3716  preq12b  3729  iinss2  3895  disjxiun  3960  trint0  4070  dtru  4139  sspwb  4161  copsexg  4189  pocl  4258  pofun  4267  solin  4274  frss  4297  tz7.7  4355  ordtri3  4365  ordtr2  4373  suc11  4433  onssneli  4439  reusv1  4471  reusv2lem1  4472  alxfr  4484  ralxfrALT  4490  iunpw  4507  ordom  4602  limom  4608  peano5  4616  2optocl  4718  3optocl  4719  ssrel  4729  ssrelrel  4740  relop  4787  asymref2  5013  xpidtr  5018  trin2  5019  sotri3  5026  poltletr  5031  xp11  5064  relcnvtr  5144  funmo  5175  fss  5300  fv3  5439  tz6.12-1  5442  tz6.12c  5446  tz6.12i  5447  mpteqb  5513  fornex  5649  funfvima  5652  fvclss  5659  f1fveq  5685  isoselem  5737  oprabid  5781  ovg  5885  poxp  6126  soxp  6127  tposfn2  6155  sorpsscmpl  6187  iotaval  6201  onnseq  6294  smoel  6310  smogt  6317  smoiso2  6319  tfrlem2  6325  tfr3  6348  tz7.48-2  6387  tz7.48-3  6389  tz7.49  6390  abianfp  6404  oecl  6469  oaordex  6489  oalimcl  6491  oaass  6492  omordi  6497  omlimcl  6509  odi  6510  omeulem1  6513  oen0  6517  oewordri  6523  nnawordi  6552  nnaass  6553  nnmordi  6562  omabs  6578  omsmolem  6584  iiner  6664  2ecoptocl  6682  3ecoptocl  6683  th3qlem2  6698  undifixp  6785  xpdom2  6890  xpf1o  6956  infensuc  6972  php  6978  onomeneq  6983  isinf  7009  findcard2  7031  unblem2  7043  finsschain  7095  marypha1  7120  hartogs  7192  card2on  7201  card2inf  7202  xpwdomg  7232  elirrv  7244  inf3lem1  7262  inf3lem2  7263  inf3lem3  7264  inf3lem5  7266  noinfep  7293  noinfepOLD  7294  trcl  7343  en3lp  7351  tcel  7363  r1sdom  7379  rankonidlem  7433  scottex  7488  pr2ne  7568  dif1card  7571  fodomnum  7617  cardaleph  7649  kmlem4  7712  kmlem9  7717  kmlem12  7720  kmlem13  7721  cflim2  7822  cfsmolem  7829  infpssrlem3  7864  isfin7-2  7955  fin1a2lem6  7964  fin1a2lem10  7968  fin1a2lem12  7970  domtriomlem  8001  axdc3lem4  8012  axdc4lem  8014  zorn2lem3  8058  zorn2lem4  8059  zorn2lem5  8060  zorn2lem6  8061  zorn2lem7  8062  zornn0g  8065  axdclem  8079  axdclem2  8080  ondomon  8118  alephval2  8127  cfpwsdom  8139  wunr1om  8274  wuncval2  8302  tskr1om  8322  grupr  8352  gruiun  8354  ingru  8370  grothomex  8384  indpi  8464  nqereu  8486  genpnnp  8562  prlem934  8590  ltaddpr2  8592  reclem2pr  8605  mulgt0sr  8660  supsrlem  8666  lemul1a  9543  squeeze0  9592  peano5nni  9682  nnunb  9893  fzind  10041  nn0ind-raph  10044  zindd  10045  eluzadd  10188  uzin  10192  xmulasslem  10536  icoshft  10689  fzen  10742  expcllem  11045  expeq0  11063  mulexp  11072  leexp2r  11090  bernneq  11158  facdiv  11231  hashmap  11317  cjexp  11565  absexp  11719  iseraltlem2  12085  sin01gt0  12397  alzdvds  12505  dvdslegcd  12622  gcdneg  12632  rplpwr  12662  qredeq  12712  prmpwdvds  12878  prmreclem4  12893  ramcl  13003  imasleval  13370  mreiincl  13425  mreexexd  13477  drsdirfi  13999  spwmo  14262  efgi2  14961  fiinopn  16574  tgcl  16634  distop  16660  isclo2  16752  iscldtop  16759  ssnei2  16780  opnnei  16784  pnfnei  16877  mnfnei  16878  tgcnp  16910  cnpnei  16920  2ndcctbss  17108  1stcelcls  17114  txcnpi  17229  cnmptcom  17299  fbfinnfr  17463  isfildlem  17479  snfil  17486  fbunfip  17491  fgcl  17500  elfm2  17570  fmfnfmlem1  17576  fmco  17583  fbflim2  17599  flffbas  17617  cnpflf2  17622  flimfcls  17648  tmdgsum  17705  neibl  17974  metcnp3  18013  fgcfil  18624  caubl  18660  volsuplem  18839  ellimc3  19156  dvnadd  19205  dvnres  19207  cpnord  19211  dvnfre  19228  mpfrcl  19329  ply1divex  19449  aalioulem2  19640  cxpmul2  19963  wilthlem3  20235  lgsquad2lem2  20525  qabvexp  20702  gxnn0add  20866  gxnn0mul  20869  ismgm  20912  isexid2  20917  ipassi  21344  ubthlem2  21375  isch3  21746  shintcli  21833  shmodsi  21893  spansncvi  22174  pjjsi  22222  hoaddsub  22321  eigorthi  22342  pjss2coi  22669  pjnormssi  22673  pj3cor1i  22714  strb  22763  dmdmd  22805  mdsl0  22815  csmdsymi  22839  chrelat2i  22870  cvati  22871  mdsymlem3  22910  mdsymlem6  22913  sumdmdlem2  22924  dmdbr5ati  22927  cvmlift2lem1  23170  3ccased  23410  dedekind  23418  dfres3  23452  dfon2lem3  23475  rdgprc  23485  trpredmintr  23568  trpredrec  23575  wfr3g  23589  wfrlem12  23601  frr3g  23614  frrlem11  23627  sltval2  23643  axfelem13  23692  elfuns  23794  axcontlem4  23935  cgrextend  23971  btwndiff  23990  btwnconn1lem12  24061  brsegle  24071  broutsideof2  24085  funray  24103  meran1  24190  waj-ax  24193  arg-ax  24195  wl-pm2.86i  24261  isunscov  24405  restidsing  24407  twsymr  24409  prj1b  24410  prj3  24411  fixpc  24425  domintrefc  24457  mapmapmap  24480  injsurinj  24481  repfuntw  24492  cbcpcp  24494  prl  24499  prl2  24501  prjmapcp2  24502  dstr  24503  jidd  24524  midd  24525  int2pre  24569  ubpar  24593  inposet  24610  tolat  24618  toplat  24622  latdir  24627  ridlideq  24667  rzrlzreq  24668  resgcom  24683  grpodivone  24705  grpodivfo  24706  rltrran  24746  zerdivemp1  24768  muldisc  24813  svli2  24816  svs2  24819  truni1  24837  truni2  24838  truni3  24839  inttop2  24847  nsn  24862  intopcoaconlem3b  24870  intopcoaconc  24873  qusp  24874  intcont  24875  prcnt  24883  fisub  24886  cmptdst  24900  exopcopn  24904  prdnei  24905  limptlimpr2lem1  24906  limptlimpr2lem2  24907  islimrs  24912  islimrs3  24913  islimrs4  24914  bwt2  24924  iintlem1  24942  iint  24944  lvsovso  24958  supnuf  24961  claddrvr  24980  sigadd  24981  addcomv  24987  addcanrg  24999  negveudr  25001  subclrvd  25006  distsava  25021  intvconlem1  25035  hdrmp  25038  cmppfd  25077  domcmpd  25078  codcmpd  25079  cmpasso  25105  cmpida  25106  cmpidb  25107  cmpassoh  25133  homgrf  25134  imonclem  25145  cmpmon  25147  iepiclem  25155  isepic  25156  idfisf  25173  issrc  25199  propsrc  25200  partarelt1  25228  inttarcar  25233  fnctartar  25239  fnctartar2  25240  prismorcset2  25250  cmpmor  25307  setiscat  25311  lemindclsbu  25327  indcls2  25328  clscnc  25342  pgapspf2  25385  gltpntl  25404  lineval5a  25420  lineval6a  25421  isconcl5a  25433  isconcl5ab  25434  isconcl6a  25435  isibg2aa  25444  isib2g1a1  25448  isibg1a2  25449  isibg2a  25450  isibg1a3a  25454  isibg1a4a  25455  isibg1a5a  25456  bsstr  25460  nbssntr  25461  sgplpte21d  25468  segline  25473  pxysxy  25474  lppotoslem  25475  lppotos  25476  xsyysx  25477  nbssntrs  25479  pdiveql  25500  abhp  25505  elicc3  25560  nn0prpwlem  25570  nn0prpw  25571  fnessref  25625  neibastop2lem  25641  filnetlem4  25662  fzmul  25775  fdc  25787  seqpo  25789  incsequz  25790  isismty  25857  ismtybndlem  25862  heibor1lem  25865  ghomco  25905  zerdivemp1x  25918  pridlc  26028  ceqsex3OLD  26058  nelss  26083  incssnn0  26118  fphpd  26231  jm2.19lem3  26416  setindtr  26449  dfac21  26496  islssfg2  26501  mpaaeu  26687  psgnunilem4  26752  pm14.24  26965  stoweidlem26  27075  hirstL-ax3  27114  sb5ALT  27304  truniALT  27321  onfrALTlem3  27325  ee223  27419  3orbi123VD  27639  sbc3orgVD  27640  exbirVD  27642  exbiriVD  27643  sbcim2gVD  27664  trsbcVD  27666  truniALTVD  27667  onfrALTlem3VD  27676  onfrALTlem2VD  27678  csbrngVD  27685  19.41rgVD  27691  a9e2eqVD  27696  a9e2ndeqVD  27698  2uasbanhVD  27700  sb5ALTVD  27702  vk15.4jVD  27703  equequ2K  28118  a4eimfK  28127  a4imfK  28128  a4imK  28129  a4imvK  28130  ax12olem21K  28201  ax12olem21X  28202  ax12olem22K  28204  ax12olem23aK  28206  ax12olem23X  28207  ax10lem16X  28215  ax10lem26X  28225  ax10X  28227  ax12-3  28234  ax9lem2  28271  ax9lem5  28274  ax9lem15  28284  ax9vax9  28288  cdleme18d  29614  tendovalco  30084  cdlemn11pre  30530  dihord2pre  30545
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator