MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com12 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  430  imdistanri  667  pm2.64  728  pm2.75  786  ccased  879  dedlem0b  885  3impd  1130  3expd  1133  mp3an1i  1234  simplbi2com  1315  meredith  1319  ax12olem21  1565  ax12olem23  1567  ax10lem16  1575  ax10lem26  1585  ax10  1587  hbimd  1680  19.21t  1683  equtrr  1701  sbequ2  1755  ax11b  1801  sb6rf  1843  sb56  1849  exmoeu  2003  moimv  2009  eupickbi  2027  2eu1  2041  exists2  2051  r19.12  2415  2gencl  2540  3gencl  2541  rcla4cv  2595  ceqex  2610  mob  2667  euind  2672  reuind  2686  sseq2  2873  uneqdifeq  3197  difsn  3402  eqsn  3420  preq12b  3433  intab  3532  iinss2  3593  trint0  3734  dtru  3802  sspwb  3822  copsexg  3850  pocl  3916  pofun  3925  solin  3932  frss  3955  tz7.7  4013  ordtri3  4023  ordtr2  4031  suc11  4089  onssneli  4095  eusv2  4139  ralxfrALT  4163  iunpw  4181  ordom  4276  limom  4282  peano5  4290  2optocl  4392  3optocl  4393  ssrel  4403  ssrelrel  4413  relop  4460  xpidtr  4690  trin2  4691  sotri3  4698  poltletr  4703  xp11  4736  relcnvtr  4816  funmo  4845  fss  4969  fv3  5104  tz6.12-1  5107  tz6.12c  5111  tz6.12i  5112  mpteqb  5174  fornex  5243  funfvima  5309  fvclss  5316  f1fveq  5341  isotr  5381  isotrALT  5382  isoselem  5387  oprabid  5428  ovg  5525  poxp  5756  soxp  5757  tposfn2  5783  sorpsscmpl  5811  iotaval  5825  onnseq  5860  smores  5868  smoel  5876  smogt  5883  smoiso2  5885  tfrlem2  5891  tfr3  5914  tz7.48-2  5953  tz7.48-3  5955  tz7.49  5956  abianfp  5970  oecl  6035  oaordex  6055  oalimcl  6057  oaass  6058  omordi  6063  omlimcl  6075  odi  6076  omeulem1  6079  oen0  6083  oewordri  6089  nnawordi  6118  nnaass  6119  nnmordi  6128  omabs  6144  omsmolem  6150  iiner  6230  2ecoptocl  6238  3ecoptocl  6239  th3qlem2  6254  undifixp  6334  xpdom2  6438  xpf1o  6551  infensuc  6567  php  6573  onomeneq  6578  isinf  6603  findcard2  6625  unblem2  6637  finsschain  6688  marypha1  6713  supub  6734  suplub  6735  supsnALT  6750  hartogs  6786  card2on  6795  card2inf  6796  xpwdomg  6826  elirrv  6838  inf3lem1  6856  inf3lem2  6857  inf3lem3  6858  inf3lem5  6860  noinfep  6887  noinfepOLD  6888  trcl  6937  en3lp  6945  tcel  6957  r1sdom  6973  rankonidlem  7026  scottex  7081  pr2ne  7161  dif1card  7164  fodomnum  7210  cardaleph  7242  cflim2  7396  cfsmolem  7403  infpssrlem3  7438  isfin7-2  7529  fin1a2lem6  7538  fin1a2lem10  7542  fin1a2lem12  7544  domtriomlem  7575  axdc3lem4  7586  axdc4lem  7588  kmlem4  7626  kmlem9  7631  kmlem12  7634  kmlem13  7635  zorn2lem3  7645  zorn2lem4  7646  zorn2lem5  7647  zorn2lem6  7648  zorn2lem7  7649  zornn0g  7652  axdclem  7666  axdclem2  7667  ondomon  7703  alephval2  7710  cfpwsdom  7722  axrepnd  7732  tskr1om  7857  grupr  7885  gruiun  7887  ingru  7902  grothomex  7916  indpi  7996  nqereu  8018  genpnnp  8094  prlem934  8122  ltaddpr2  8124  reclem2pr  8137  mulgt0sr  8192  supsrlem  8198  lemul1a  9036  squeeze0  9085  peano5nni  9174  nnunb  9383  fzind  9531  nn0ind-raph  9534  zindd  9535  eluzadd  9678  uzin  9682  xmulasslem  10026  icoshft  10176  fzen  10227  expcllem  10522  expeq0  10540  mulexp  10549  leexp2r  10567  bernneq  10634  facdiv  10707  hashmap  10793  cjexp  10883  absexp  11035  iseraltlem2  11400  sin01gt0  11707  alzdvds  11814  dvdslegcd  11854  gcdneg  11864  rplpwr  11894  qredeq  11944  prmpwdvds  12110  prmreclem4  12125  ramcl  12235  imasleval  12582  mreiincl  12635  drsdirfi  12687  spwmo  12941  efgi2  13798  fiinopn  15408  tgcl  15468  distop  15494  isclo2  15585  iscldtop  15592  ssnei2  15613  opnnei  15617  pnfnei  15696  mnfnei  15697  tgcnp  15729  cnpnei  15739  2ndcctbss  15923  1stcelcls  15929  txcnpi  16044  cnmptcom  16114  fbfinnfr  16278  isfildlem  16294  snfil  16301  fbunfip  16306  fgcl  16315  elfm2  16385  fmfnfmlem1  16391  fmco  16398  fbflim2  16414  flffbas  16432  cnpflf2  16437  flimfcls  16463  tmdgsum  16520  neibl  16790  metcnp3  16829  fgcfil  17432  caubl  17468  volsuplem  17647  dvnadd  17989  dvnres  17990  cpnord  17994  mpfrcl  18102  ply1divex  18220  cxpmul2  18681  wilthlem3  18917  lgsquad2lem2  19207  qabvexp  19384  gxnn0add  19531  gxnn0mul  19534  ismgm  19577  isexid2  19582  ipassi  20009  ubthlem2  20040  isch3  20411  shintcli  20498  shmodsi  20558  spansncvi  20839  pjjsi  20887  hoaddsub  20986  eigorthi  21007  pjss2coi  21334  pjnormssi  21338  pj3cor1i  21379  strb  21428  dmdmd  21470  mdsl0  21480  csmdsymi  21504  chrelat2i  21535  cvati  21536  mdsymlem3  21575  mdsymlem6  21578  sumdmdlem2  21589  dmdbr5ati  21592  cvmlift2lem1  21764  3ccased  22007  dedekind  22011  dfres3  22043  dfon2lem3  22066  rdgprc  22076  trpredmintr  22160  trpredrec  22167  wfr3g  22181  wfrlem12  22193  frr3g  22206  frrlem11  22219  sltval2  22235  axfelem13  22284  elfuns  22386  axcontlem4  22527  cgrextend  22563  btwndiff  22582  btwnconn1lem12  22653  brsegle  22663  broutsideof2  22677  funray  22695  meran1  22757  waj-ax  22760  arg-ax  22762  wl-pm2.86i  22828  copsexgb  22865  evpexun  22894  isunscov  22954  restidsing  22956  twsymr  22958  prj1b  22959  prj3  22960  fixpc  22974  domintrefc  23006  mapmapmap  23031  injsurinj  23032  repfuntw  23043  cbcpcp  23045  prl  23050  prl2  23052  prjmapcp2  23053  dstr  23054  jidd  23075  midd  23076  int2pre  23120  ubpar  23144  inposet  23161  tolat  23169  toplat  23173  latdir  23178  ridlideq  23218  rzrlzreq  23219  resgcom  23234  grpodivone  23256  grpodivfo  23257  rltrran  23297  zerdivemp1  23319  muldisc  23367  svli2  23370  svs2  23373  truni1  23391  truni2  23392  truni3  23393  inttop2  23404  nsn  23419  intopcoaconlem3b  23427  intopcoaconc  23430  qusp  23431  intcont  23432  prcnt  23440  fisub  23443  cmptdst  23457  exopcopn  23461  prdnei  23462  limptlimpr2lem1  23463  limptlimpr2lem2  23464  islimrs  23469  islimrs3  23470  islimrs4  23471  bwt2  23481  iintlem1  23499  iint  23501  lvsovso  23515  supnuf  23518  claddrvr  23537  sigadd  23538  addcomv  23544  addcanrg  23556  negveudr  23558  subclrvd  23563  distsava  23578  intvconlem1  23592  hdrmp  23595  cmppfd  23634  domcmpd  23635  codcmpd  23636  cmpasso  23662  cmpida  23663  cmpidb  23664  cmpassoh  23690  homgrf  23691  imonclem  23702  cmpmon  23704  iepiclem  23712  isepic  23713  idfisf  23730  issrc  23756  propsrc  23757  partarelt1  23785  inttarcar  23790  fnctartar  23796  fnctartar2  23797  prismorcset2  23807  cmpmor  23864  setiscat  23868  lemindclsbu  23885  indcls2  23886  clscnc  23900  pgapspf2  23943  gltpntl  23962  lineval5a  23978  lineval6a  23979  isconcl5a  23992  isconcl5ab  23993  isconcl6a  23994  isibg2aa  24003  isib2g1a1  24007  isibg1a2  24008  isibg2a  24009  isibg1a3a  24013  isibg1a4a  24014  isibg1a5a  24015  bsstr  24019  nbssntr  24020  sgplpte21d  24027  segline  24032  pxysxy  24033  lppotoslem  24034  lppotos  24035  xsyysx  24036  nbssntrs  24038  pdiveql  24059  abhp  24064  elicc3  24120  nn0prpwlem  24130  nn0prpw  24131  fnessref  24185  neibastop2lem  24201  filnetlem4  24222  fzmul  24336  fdc  24348  seqpo  24350  incsequz  24351  isismty  24418  ismtybndlem  24423  heibor1lem  24426  ghomco  24466  zerdivemp1x  24479  pridlc  24589  ceqsex3OLD  24619  nelss  24644  incssnn0  24681  fphpd  24791  jm2.19lem3  24976  setindtr  25009  dfac21  25060  aalioulem2  25074  islssfg2  25104  mpaaeu  25290  psgnunilem4  25355  pm14.24  25569  hirstL-ax3  25622  sb5ALT  25739  truniALT  25756  onfrALTlem3  25760  ee223  25853  3orbi123VD  26026  sbc3orgVD  26027  exbirVD  26029  exbiriVD  26030  sbcim2gVD  26051  trsbcVD  26053  truniALTVD  26054  onfrALTlem3VD  26063  onfrALTlem2VD  26065  csbrngVD  26072  19.41rgVD  26078  a9e2eqVD  26083  a9e2ndeqVD  26085  2uasbanhVD  26087  sb5ALTVD  26089  vk15.4jVD  26090  ax12-3  26507  ax9lem2  26544  ax9lem5  26547  ax9lem15  26557  ax9vax9  26561  cdleme18d  27887  tendovalco  28357  cdlemn11pre  28803  dihord2pre  28818
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator