MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com12 Unicode version

Theorem com12 28
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 27 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 5
This theorem is referenced by:  syl5  29  syl6com  32  mpcom  33  syli  34  pm2.27  36  pm2.43b  47  syl9r  68  com3r  74  pm2.86i  93  pm2.24  101  con3rr3  127  expt  147  jad  153  pm2.61  162  syl5ibcom  210  syl5ibrcom  212  pm5.501  329  jaod  368  orel1  370  pm2.62  397  impcom  417  imp3a  418  expcom  422  exp3a  423  pm3.21  431  imdistanri  669  pm2.64  761  pm2.75  819  ccased  912  dedlem0b  918  3impd  1164  3expd  1167  mp3an1i  1269  simplbi2com  1359  meredith  1389  ax12olem21  1644  ax12olem23  1646  ax10lem16  1654  ax10lem26  1664  ax10  1666  hbimd  1798  equtrr  1816  sbequ2  1879  ax11b  1930  sb6rf  1973  sb56  1979  mo  2123  exmoeu  2143  moimv  2149  eupickbi  2167  2mo  2179  2eu1  2181  exists2  2191  r19.12  2604  2gencl  2740  3gencl  2741  rcla4cv  2803  ceqex  2820  mob  2869  euind  2874  reuind  2888  sseq2  3101  reupick2  3341  uneqdifeq  3428  difsn  3637  eqsn  3655  preq12b  3668  iinss2  3832  disjxiun  3897  trint0  4006  dtru  4074  sspwb  4096  copsexg  4124  pocl  4193  pofun  4202  solin  4209  frss  4232  tz7.7  4290  ordtri3  4300  ordtr2  4308  suc11  4366  onssneli  4372  reusv1  4404  reusv2lem1  4405  alxfr  4417  ralxfrALT  4423  iunpw  4440  ordom  4535  limom  4541  peano5  4549  2optocl  4651  3optocl  4652  ssrel  4662  ssrelrel  4673  relop  4720  asymref2  4946  xpidtr  4951  trin2  4952  sotri3  4959  poltletr  4964  xp11  4997  relcnvtr  5077  funmo  5108  fss  5232  fv3  5368  tz6.12-1  5371  tz6.12c  5375  tz6.12i  5376  mpteqb  5441  fornex  5577  funfvima  5580  fvclss  5587  f1fveq  5613  isoselem  5665  oprabid  5709  ovg  5812  poxp  6053  soxp  6054  tposfn2  6082  sorpsscmpl  6114  iotaval  6128  onnseq  6221  smoel  6237  smogt  6244  smoiso2  6246  tfrlem2  6252  tfr3  6275  tz7.48-2  6314  tz7.48-3  6316  tz7.49  6317  abianfp  6331  oecl  6396  oaordex  6416  oalimcl  6418  oaass  6419  omordi  6424  omlimcl  6436  odi  6437  omeulem1  6440  oen0  6444  oewordri  6450  nnawordi  6479  nnaass  6480  nnmordi  6489  omabs  6505  omsmolem  6511  iiner  6591  2ecoptocl  6609  3ecoptocl  6610  th3qlem2  6625  undifixp  6712  xpdom2  6816  xpf1o  6882  infensuc  6898  php  6904  onomeneq  6909  isinf  6935  findcard2  6957  unblem2  6969  finsschain  7020  marypha1  7045  hartogs  7117  card2on  7126  card2inf  7127  xpwdomg  7157  elirrv  7169  inf3lem1  7187  inf3lem2  7188  inf3lem3  7189  inf3lem5  7191  noinfep  7218  noinfepOLD  7219  trcl  7268  en3lp  7276  tcel  7288  r1sdom  7304  rankonidlem  7358  scottex  7413  pr2ne  7493  dif1card  7496  fodomnum  7542  cardaleph  7574  kmlem4  7637  kmlem9  7642  kmlem12  7645  kmlem13  7646  cflim2  7747  cfsmolem  7754  infpssrlem3  7789  isfin7-2  7880  fin1a2lem6  7889  fin1a2lem10  7893  fin1a2lem12  7895  domtriomlem  7926  axdc3lem4  7937  axdc4lem  7939  zorn2lem3  7983  zorn2lem4  7984  zorn2lem5  7985  zorn2lem6  7986  zorn2lem7  7987  zornn0g  7990  axdclem  8004  axdclem2  8005  ondomon  8041  alephval2  8048  cfpwsdom  8060  wunr1om  8195  wuncval2  8223  tskr1om  8243  grupr  8273  gruiun  8275  ingru  8291  grothomex  8305  indpi  8385  nqereu  8407  genpnnp  8483  prlem934  8511  ltaddpr2  8513  reclem2pr  8526  mulgt0sr  8581  supsrlem  8587  lemul1a  9430  squeeze0  9479  peano5nni  9569  nnunb  9779  fzind  9927  nn0ind-raph  9930  zindd  9931  eluzadd  10074  uzin  10078  xmulasslem  10422  icoshft  10575  fzen  10626  expcllem  10929  expeq0  10947  mulexp  10956  leexp2r  10974  bernneq  11041  facdiv  11114  hashmap  11200  cjexp  11448  absexp  11600  iseraltlem2  11966  sin01gt0  12278  alzdvds  12386  dvdslegcd  12503  gcdneg  12513  rplpwr  12543  qredeq  12593  prmpwdvds  12759  prmreclem4  12774  ramcl  12884  imasleval  13251  mreiincl  13304  drsdirfi  13762  spwmo  14016  efgi2  14715  fiinopn  16325  tgcl  16385  distop  16411  isclo2  16503  iscldtop  16510  ssnei2  16531  opnnei  16535  pnfnei  16628  mnfnei  16629  tgcnp  16661  cnpnei  16671  2ndcctbss  16859  1stcelcls  16865  txcnpi  16980  cnmptcom  17050  fbfinnfr  17214  isfildlem  17230  snfil  17237  fbunfip  17242  fgcl  17251  elfm2  17321  fmfnfmlem1  17327  fmco  17334  fbflim2  17350  flffbas  17368  cnpflf2  17373  flimfcls  17399  tmdgsum  17456  neibl  17725  metcnp3  17764  fgcfil  18375  caubl  18411  volsuplem  18590  ellimc3  18907  dvnadd  18956  dvnres  18958  cpnord  18962  dvnfre  18979  mpfrcl  19080  ply1divex  19200  aalioulem2  19391  cxpmul2  19722  wilthlem3  19958  lgsquad2lem2  20248  qabvexp  20425  gxnn0add  20572  gxnn0mul  20575  ismgm  20618  isexid2  20623  ipassi  21050  ubthlem2  21081  isch3  21452  shintcli  21539  shmodsi  21599  spansncvi  21880  pjjsi  21928  hoaddsub  22027  eigorthi  22048  pjss2coi  22375  pjnormssi  22379  pj3cor1i  22420  strb  22469  dmdmd  22511  mdsl0  22521  csmdsymi  22545  chrelat2i  22576  cvati  22577  mdsymlem3  22616  mdsymlem6  22619  sumdmdlem2  22630  dmdbr5ati  22633  cvmlift2lem1  22805  3ccased  23045  dedekind  23053  dfres3  23092  dfon2lem3  23115  rdgprc  23125  trpredmintr  23208  trpredrec  23215  wfr3g  23229  wfrlem12  23241  frr3g  23254  frrlem11  23267  sltval2  23283  axfelem13  23332  elfuns  23434  axcontlem4  23575  cgrextend  23611  btwndiff  23630  btwnconn1lem12  23701  brsegle  23711  broutsideof2  23725  funray  23743  meran1  23830  waj-ax  23833  arg-ax  23835  wl-pm2.86i  23901  isunscov  24045  restidsing  24047  twsymr  24049  prj1b  24050  prj3  24051  fixpc  24065  domintrefc  24097  mapmapmap  24120  injsurinj  24121  repfuntw  24132  cbcpcp  24134  prl  24139  prl2  24141  prjmapcp2  24142  dstr  24143  jidd  24164  midd  24165  int2pre  24209  ubpar  24233  inposet  24250  tolat  24258  toplat  24262  latdir  24267  ridlideq  24307  rzrlzreq  24308  resgcom  24323  grpodivone  24345  grpodivfo  24346  rltrran  24386  zerdivemp1  24408  muldisc  24453  svli2  24456  svs2  24459  truni1  24477  truni2  24478  truni3  24479  inttop2  24487  nsn  24502  intopcoaconlem3b  24510  intopcoaconc  24513  qusp  24514  intcont  24515  prcnt  24523  fisub  24526  cmptdst  24540  exopcopn  24544  prdnei  24545  limptlimpr2lem1  24546  limptlimpr2lem2  24547  islimrs  24552  islimrs3  24553  islimrs4  24554  bwt2  24564  iintlem1  24582  iint  24584  lvsovso  24598  supnuf  24601  claddrvr  24620  sigadd  24621  addcomv  24627  addcanrg  24639  negveudr  24641  subclrvd  24646  distsava  24661  intvconlem1  24675  hdrmp  24678  cmppfd  24717  domcmpd  24718  codcmpd  24719  cmpasso  24745  cmpida  24746  cmpidb  24747  cmpassoh  24773  homgrf  24774  imonclem  24785  cmpmon  24787  iepiclem  24795  isepic  24796  idfisf  24813  issrc  24839  propsrc  24840  partarelt1  24868  inttarcar  24873  fnctartar  24879  fnctartar2  24880  prismorcset2  24890  cmpmor  24947  setiscat  24951  lemindclsbu  24967  indcls2  24968  clscnc  24982  pgapspf2  25025  gltpntl  25044  lineval5a  25060  lineval6a  25061  isconcl5a  25073  isconcl5ab  25074  isconcl6a  25075  isibg2aa  25084  isib2g1a1  25088  isibg1a2  25089  isibg2a  25090  isibg1a3a  25094  isibg1a4a  25095  isibg1a5a  25096  bsstr  25100  nbssntr  25101  sgplpte21d  25108  segline  25113  pxysxy  25114  lppotoslem  25115  lppotos  25116  xsyysx  25117  nbssntrs  25119  pdiveql  25140  abhp  25145  elicc3  25200  nn0prpwlem  25210  nn0prpw  25211  fnessref  25265  neibastop2lem  25281  filnetlem4  25302  fzmul  25415  fdc  25427  seqpo  25429  incsequz  25430  isismty  25497  ismtybndlem  25502  heibor1lem  25505  ghomco  25545  zerdivemp1x  25558  pridlc  25668  ceqsex3OLD  25698  nelss  25723  incssnn0  25758  fphpd  25871  jm2.19lem3  26056  setindtr  26089  dfac21  26136  islssfg2  26141  mpaaeu  26327  psgnunilem4  26392  pm14.24  26605  hirstL-ax3  26657  sb5ALT  26776  truniALT  26793  onfrALTlem3  26797  ee223  26890  3orbi123VD  27063  sbc3orgVD  27064  exbirVD  27066  exbiriVD  27067  sbcim2gVD  27088  trsbcVD  27090  truniALTVD  27091  onfrALTlem3VD  27100  onfrALTlem2VD  27102  csbrngVD  27109  19.41rgVD  27115  a9e2eqVD  27120  a9e2ndeqVD  27122  2uasbanhVD  27124  sb5ALTVD  27126  vk15.4jVD  27127  ax12-3  27540  ax9lem2  27577  ax9lem5  27580  ax9lem15  27590  ax9vax9  27594  cdleme18d  28920  tendovalco  29390  cdlemn11pre  29836  dihord2pre  29851
This theorem was proved from axioms:  ax-1 6  ax-2 7  ax-mp 9
  Copyright terms: Public domain W3C validator