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

Theorem mpcom 32
Description: Modus ponens inference with commutation of antecedents. (Contributed by NM, 17-Mar-1996.)
Hypotheses
Ref Expression
mpcom.1  |-  ( ps 
->  ph )
mpcom.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mpcom  |-  ( ps 
->  ch )

Proof of Theorem mpcom
StepHypRef Expression
1 mpcom.1 . 2  |-  ( ps 
->  ph )
2 mpcom.2 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
32com12 27 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
41, 3mpd 14 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syldan  456  ax16i  1986  ceqex  2898  limomss  4661  elimasni  5040  sotri  5070  sotriOLD  5075  relcoi1  5201  unixpid  5207  f1ocnv  5485  tz6.12c  5547  funbrfv  5561  oprabid  5882  ndmovordi  6011  unielxp  6158  smogt  6384  oawordeulem  6552  omass  6578  ecopovtrn  6761  php  7045  unxpdom  7070  findcard3  7100  isfinite2  7115  cantnfval2  7370  cantnfle  7372  cantnfp1lem3  7382  cantnflem1  7391  cnfcom  7403  rankr1ai  7470  rankonidlem  7500  rankxplim2  7550  oncard  7593  ficardom  7594  cardne  7598  acnnum  7679  alephord2i  7704  cardaleph  7716  aceq3lem  7747  dfac5lem5  7754  dfac12lem3  7771  cdainf  7818  ackbij1lem16  7861  cfslb  7892  cfslb2n  7894  cfsmolem  7896  fin4i  7924  infpssr  7934  fin1a2lem6  8031  axdc3lem2  8077  axcclem  8083  ttukeylem6  8141  fodomb  8151  gchi  8246  fpwwe2lem5  8256  pwfseqlem4  8284  pwfseq  8286  inawina  8312  wunfi  8343  inar1  8397  ltexnq  8599  ltbtwnnq  8602  ltexprlem4  8663  ltexpri  8667  prlem936  8671  suplem1pr  8676  suplem2pr  8677  recexsrlem  8725  mulgt0sr  8727  map2psrpr  8732  supsr  8734  ledivp1i  9682  nnind  9764  nnmulcl  9769  nnnegz  10027  uzindOLD  10106  ublbneg  10302  xmulasslem  10605  ixxssixx  10670  iccshftri  10770  iccshftli  10772  iccdili  10774  icccntri  10776  seqp1  11061  seqcl2  11064  seqfveq2  11068  seqshft2  11072  monoord  11076  seqsplit  11079  seqcaopr3  11081  seqf1olem2a  11084  seqf1o  11087  seqid2  11092  seqhomo  11093  hashf1lem2  11394  seqcoll  11401  cjre  11624  climeu  12029  climub  12135  fsum2d  12234  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  ruclem9  12516  sadcadd  12649  sadadd2  12651  saddisjlem  12655  smuval2  12673  smupval  12679  smueqlem  12681  smumullem  12683  exprmfct  12789  eulerthlem2  12850  pcmpt  12940  vdwlem10  13037  prmlem1a  13108  mreexexd  13550  letsr  14349  sylow1lem1  14909  efginvrel2  15036  efgsrel  15043  gsum2d  15223  dprdval  15238  ablfac1eulem  15307  pgpfac1  15315  pgpfac  15319  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  tg2  16703  neindisj2  16860  t1t0  17076  fiuncmp  17131  hmeof1o  17455  ist1-5lem  17511  t1r0  17512  alexsublem  17738  imasdsf1olem  17937  tgioo  18302  fsumcn  18374  voliunlem3  18909  itgfsum  19181  dvbsss  19252  dvmptfsum  19322  dvfsumlem2  19374  dvfsumlem4  19376  mpfaddcl  19426  mpfmulcl  19427  pf1addcl  19436  pf1mulcl  19437  plyco  19623  dgrcolem1  19654  dgrco  19656  dvntaylp  19750  taylthlem1  19752  jensen  20283  bposlem5  20527  lgsquad2lem2  20598  dchrisum0flb  20659  pntpbnd1  20735  pntlemf  20754  opidon2  20991  isexid2  20992  grpomndo  21013  elghomlem2  21029  rngoidmlem  21090  rngoueqz  21097  blocn2  21386  cvexchlem  22948  cdj3lem2b  23017  issgon  23484  subfacp1lem6  23716  cvmliftlem7  23822  cvmliftlem10  23825  eupath2  23904  relexp0  24025  relexpsucr  24026  relexpsucl  24028  relexprel  24031  relexpdm  24032  relexprn  24033  relexpadd  24035  relexpindlem  24036  relexpind  24037  rtrclreclem.trans  24043  rtrclreclem.min  24044  dfrtrcl2  24045  rtrclind  24046  pprodss4v  24424  funpartfv  24483  brbtwn  24527  brcgr  24528  segleantisym  24738  rankeq1o  24801  inpws1  25042  mapmapmap  25148  injsurinj  25149  prl  25167  prl2  25169  sege  25252  mxlmnl2  25270  defse3  25272  dfps2  25289  ablocomgrp  25342  grpodivfo  25374  grpodrcan  25375  grpodlcan  25376  rngodmeqrn  25419  mulinvsca  25480  glmrngo  25482  svs2  25487  truni2  25506  truni3  25507  intopcoaconlem3b  25538  intcont  25543  fil2ss  25557  prdnei  25573  limptlimpr2lem1  25574  islimrs4  25582  bwt2  25592  xrletr2  25618  lvsovso  25626  supnuf  25629  addcanrg  25667  negveud  25668  negveudr  25669  subctct  25854  tartarmap  25888  inttarcar  25901  carinttar  25902  fnctartar  25907  fnctartar2  25908  codcatfun  25934  grphidmor2  25953  cmp2morp  25958  cmp2morpcatt  25962  setiscat  25979  indcls2  25996  clscnc  26010  lineval5a  26088  lineval6a  26089  isconcl6a  26103  isconcl6ab  26104  isibg2aa  26112  isib2g1a1  26116  isibg2a  26118  isibg1a3a  26122  isibg1spa  26123  isibg1a5a  26124  bsstr  26128  nbssntr  26129  lppotoslem  26143  lppotos  26144  nbssntrs  26147  abhp  26173  mettrifi  26473  iscringd  26624  mzpadd  26816  mzpmul  26817  mzpcompact2  26830  dford3lem2  27120  aomclem6  27156  cnsrexpcl  27370  pmtrfrn  27400  ax10ext  27606  iotavalsb  27633  fmul01  27710  fmulcl  27711  fmuldfeqlem1  27712  fmuldfeq  27713  stoweidlem2  27751  stoweidlem3  27752  stoweidlem17  27766  stoweidlem21  27770  stoweidlem26  27775  stoweidlem31  27780  stoweidlem34  27783  stoweidlem48  27797  funressnfv  27991  afv0fv0  28012  afv0nbfvbi  28014  uslisumgra  28112  usisuslgra  28113  usgra0v  28117  usgra1v  28126  nbusgra  28143  iscusgra0  28154  cusgrauvtx  28168  3vfriswmgra  28183  bnj938  28969  bnj964  28975  bnj1052  29005  bnj1125  29022  cdlemk35s  31126  cdlemk39s  31128  cdlemk42  31130
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator