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  101  con3rr3  128  expt  148  jad  154  pm2.61  163  syl5ibcom  211  syl5ibrcom  213  pm5.501  330  jaod  369  orel1  371  pm2.62  398  impcom  419  imp3a  420  expcom  424  exp3a  425  pm3.21  435  imdistanri  672  pm2.64  764  pm2.75  822  ccased  913  dedlem0b  919  3impd  1165  3expd  1168  mp3an1i  1270  simplbi2com  1364  meredith  1394  sbequ2  1631  equtrr  1653  ax12olem1  1868  ax12olem3  1870  ax10lem4  1881  ax11b  1935  sb6rf  2031  sb56  2037  exsb  2069  mo  2165  exmoeu  2185  morimv  2191  eupickbi  2209  2mo  2221  2eu1  2223  exists2  2233  r19.12  2656  2gencl  2817  3gencl  2818  rspccv  2881  ceqex  2898  mob  2947  euind  2952  reuind  2968  2rmorex  2969  sseq2  3200  reupick2  3454  uneqdifeq  3542  difsn  3755  eqsn  3775  preq12b  3788  iinss2  3954  disjxiun  4020  trint0  4130  dtru  4201  sspwb  4223  copsexg  4252  pocl  4321  pofun  4330  solin  4337  frss  4360  tz7.7  4418  ordtri3  4428  ordtr2  4436  suc11  4496  onssneli  4502  reusv1  4534  reusv2lem1  4535  alxfr  4547  ralxfrALT  4553  iunpw  4570  ordom  4665  limom  4671  peano5  4679  2optocl  4765  3optocl  4766  ssrel  4776  ssrelrel  4787  relop  4834  asymref2  5060  xpidtr  5065  trin2  5066  sotri3  5073  poltletr  5078  xp11  5111  relcnvtr  5192  iotaval  5230  funmo  5271  fss  5397  fv3  5541  tz6.12c  5547  tz6.12i  5548  mpteqb  5614  fornex  5750  funfvima  5753  fvclss  5760  f1fveq  5786  isoselem  5838  oprabid  5882  ovg  5986  poxp  6227  soxp  6228  tposfn2  6256  sorpsscmpl  6288  onnseq  6361  smoel  6377  smogt  6384  smoiso2  6386  tfrlem2  6392  tfr3  6415  tz7.48-2  6454  tz7.48-3  6456  tz7.49  6457  abianfp  6471  oecl  6536  oaordex  6556  oalimcl  6558  oaass  6559  omordi  6564  omlimcl  6576  odi  6577  omeulem1  6580  oen0  6584  oewordri  6590  nnawordi  6619  nnaass  6620  nnmordi  6629  omabs  6645  omsmolem  6651  iiner  6731  2ecoptocl  6749  3ecoptocl  6750  th3qlem2  6765  undifixp  6852  xpdom2  6957  xpf1o  7023  infensuc  7039  php  7045  onomeneq  7050  isinf  7076  findcard2  7098  unblem2  7110  finsschain  7162  marypha1  7187  hartogs  7259  card2on  7268  card2inf  7269  xpwdomg  7299  elirrv  7311  inf3lem1  7329  inf3lem2  7330  inf3lem3  7331  inf3lem5  7333  noinfep  7360  noinfepOLD  7361  trcl  7410  en3lp  7418  tcel  7430  r1sdom  7446  rankonidlem  7500  scottex  7555  pr2ne  7635  dif1card  7638  fodomnum  7684  cardaleph  7716  kmlem4  7779  kmlem9  7784  kmlem12  7787  kmlem13  7788  cflim2  7889  cfsmolem  7896  infpssrlem3  7931  isfin7-2  8022  fin1a2lem6  8031  fin1a2lem10  8035  fin1a2lem12  8037  domtriomlem  8068  axdc3lem4  8079  axdc4lem  8081  zorn2lem3  8125  zorn2lem4  8126  zorn2lem5  8127  zorn2lem6  8128  zorn2lem7  8129  zornn0g  8132  axdclem  8146  axdclem2  8147  ondomon  8185  alephval2  8194  cfpwsdom  8206  wunr1om  8341  wuncval2  8369  tskr1om  8389  grupr  8419  gruiun  8421  ingru  8437  grothomex  8451  indpi  8531  nqereu  8553  genpnnp  8629  prlem934  8657  ltaddpr2  8659  reclem2pr  8672  mulgt0sr  8727  supsrlem  8733  lemul1a  9610  squeeze0  9659  peano5nni  9749  nnunb  9961  fzind  10110  nn0ind-raph  10112  zindd  10113  eluzadd  10256  uzin  10260  xmulasslem  10605  icoshft  10758  fzen  10811  expcllem  11114  expeq0  11132  mulexp  11141  leexp2r  11159  bernneq  11227  facdiv  11300  hashmap  11387  cjexp  11635  absexp  11789  iseraltlem2  12155  sin01gt0  12470  alzdvds  12578  dvdslegcd  12695  gcdneg  12705  rplpwr  12735  qredeq  12785  prmpwdvds  12951  prmreclem4  12966  ramcl  13076  imasleval  13443  mreiincl  13498  mreexexd  13550  drsdirfi  14072  spwmo  14335  efgi2  15034  fiinopn  16647  tgcl  16707  distop  16733  isclo2  16825  iscldtop  16832  ssnei2  16853  opnnei  16857  pnfnei  16950  mnfnei  16951  tgcnp  16983  cnpnei  16993  2ndcctbss  17181  1stcelcls  17187  txcnpi  17302  cnmptcom  17372  fbfinnfr  17536  isfildlem  17552  snfil  17559  fbunfip  17564  fgcl  17573  elfm2  17643  fmfnfmlem1  17649  fmco  17656  fbflim2  17672  flffbas  17690  cnpflf2  17695  flimfcls  17721  tmdgsum  17778  neibl  18047  metcnp3  18086  fgcfil  18697  caubl  18733  volsuplem  18912  ellimc3  19229  dvnadd  19278  dvnres  19280  cpnord  19284  dvnfre  19301  mpfrcl  19402  ply1divex  19522  aalioulem2  19713  cxpmul2  20036  wilthlem3  20308  lgsquad2lem2  20598  qabvexp  20775  gxnn0add  20941  gxnn0mul  20944  ismgm  20987  isexid2  20992  ipassi  21419  ubthlem2  21450  isch3  21821  shintcli  21908  shmodsi  21968  spansncvi  22231  pjjsi  22279  hoaddsub  22396  eigorthi  22417  pjss2coi  22744  pjnormssi  22748  pj3cor1i  22789  strb  22838  dmdmd  22880  mdsl0  22890  csmdsymi  22914  chrelat2i  22945  cvati  22946  mdsymlem3  22985  mdsymlem6  22988  sumdmdlem2  22999  dmdbr5ati  23002  cvmlift2lem1  23833  3ccased  24073  dedekind  24082  dfres3  24116  dfon2lem3  24141  rdgprc  24151  trpredmintr  24234  trpredrec  24241  wfr3g  24255  wfrlem12  24267  frr3g  24280  frrlem11  24293  sltval2  24310  axcontlem4  24595  cgrextend  24631  btwndiff  24650  btwnconn1lem12  24721  brsegle  24731  broutsideof2  24745  funray  24763  meran1  24850  waj-ax  24853  arg-ax  24855  wl-pm2.86i  24921  isunscov  25074  restidsing  25076  twsymr  25078  prj1b  25079  prj3  25080  fixpc  25094  domintrefc  25125  mapmapmap  25148  injsurinj  25149  cbcpcp  25162  prl  25167  prl2  25169  prjmapcp2  25170  dstr  25171  jidd  25192  midd  25193  int2pre  25237  ubpar  25261  inposet  25278  tolat  25286  toplat  25290  latdir  25295  ridlideq  25335  rzrlzreq  25336  resgcom  25351  grpodivone  25373  grpodivfo  25374  rltrran  25414  zerdivemp1  25436  muldisc  25481  svli2  25484  svs2  25487  truni1  25505  truni2  25506  truni3  25507  inttop2  25515  nsn  25530  intopcoaconlem3b  25538  intopcoaconc  25541  qusp  25542  intcont  25543  prcnt  25551  fisub  25554  cmptdst  25568  exopcopn  25572  prdnei  25573  limptlimpr2lem1  25574  limptlimpr2lem2  25575  islimrs  25580  islimrs3  25581  islimrs4  25582  bwt2  25592  iintlem1  25610  iint  25612  lvsovso  25626  supnuf  25629  claddrvr  25648  sigadd  25649  addcomv  25655  addcanrg  25667  negveudr  25669  subclrvd  25674  distsava  25689  intvconlem1  25703  hdrmp  25706  cmppfd  25745  domcmpd  25746  codcmpd  25747  cmpasso  25773  cmpida  25774  cmpidb  25775  cmpassoh  25801  homgrf  25802  imonclem  25813  cmpmon  25815  iepiclem  25823  isepic  25824  idfisf  25841  issrc  25867  propsrc  25868  partarelt1  25896  inttarcar  25901  fnctartar  25907  fnctartar2  25908  prismorcset2  25918  cmpmor  25975  setiscat  25979  lemindclsbu  25995  indcls2  25996  clscnc  26010  pgapspf2  26053  gltpntl  26072  lineval5a  26088  lineval6a  26089  isconcl5a  26101  isconcl5ab  26102  isconcl6a  26103  isibg2aa  26112  isib2g1a1  26116  isibg1a2  26117  isibg2a  26118  isibg1a3a  26122  isibg1spa  26123  isibg1a5a  26124  bsstr  26128  nbssntr  26129  sgplpte21d  26136  segline  26141  pxysxy  26142  lppotoslem  26143  lppotos  26144  xsyysx  26145  nbssntrs  26147  pdiveql  26168  abhp  26173  elicc3  26228  nn0prpwlem  26238  nn0prpw  26239  fnessref  26293  neibastop2lem  26309  filnetlem4  26330  fzmul  26443  fdc  26455  seqpo  26457  incsequz  26458  isismty  26525  ismtybndlem  26530  heibor1lem  26533  ghomco  26573  zerdivemp1x  26586  pridlc  26696  ceqsex3OLD  26726  nelss  26751  incssnn0  26786  fphpd  26899  jm2.19lem3  27084  setindtr  27117  dfac21  27164  islssfg2  27169  mpaaeu  27355  psgnunilem4  27420  pm14.24  27632  stoweidlem26  27775  hirstL-ax3  27860  rexsb  27946  rexrsb  27947  2reu1  27964  afvres  28034  tz6.12-afv  28035  afvco2  28037  ndmaovdistr  28067  mpt2xopoveqd  28087  usgraeq12d  28111  usgraedgprv  28122  usgraedgrnv  28123  usgranloop  28124  usgra1v  28126  nbgraop  28140  nbusgra  28143  nbgranself2  28151  nbcusgra  28159  uvtxnbgra  28165  frgra2v  28177  frgra3vlem1  28178  frgra3vlem2  28179  3vfriswmgralem  28182  3vfriswmgra  28183  sb5ALT  28288  truniALT  28305  onfrALTlem3  28309  ee223  28406  3orbi123VD  28626  sbc3orgVD  28627  exbirVD  28629  exbiriVD  28630  sbcim2gVD  28651  trsbcVD  28653  truniALTVD  28654  onfrALTlem3VD  28663  onfrALTlem2VD  28665  csbrngVD  28672  19.41rgVD  28678  a9e2eqVD  28683  a9e2ndeqVD  28685  2uasbanhVD  28687  sb5ALTVD  28689  vk15.4jVD  28690  ax12-3  29104  ax9lem2  29141  ax9lem5  29144  ax9lem15  29154  ax9vax9  29158  cdleme18d  30484  tendovalco  30954  cdlemn11pre  31400  dihord2pre  31415
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator