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  1999  ceqex  2911  limomss  4677  elimasni  5056  sotri  5086  sotriOLD  5091  relcoi1  5217  unixpid  5223  f1ocnv  5501  tz6.12c  5563  funbrfv  5577  oprabid  5898  ndmovordi  6027  unielxp  6174  smogt  6400  oawordeulem  6568  omass  6594  ecopovtrn  6777  php  7061  unxpdom  7086  findcard3  7116  isfinite2  7131  cantnfval2  7386  cantnfle  7388  cantnfp1lem3  7398  cantnflem1  7407  cnfcom  7419  rankr1ai  7486  rankonidlem  7516  rankxplim2  7566  oncard  7609  ficardom  7610  cardne  7614  acnnum  7695  alephord2i  7720  cardaleph  7732  aceq3lem  7763  dfac5lem5  7770  dfac12lem3  7787  cdainf  7834  ackbij1lem16  7877  cfslb  7908  cfslb2n  7910  cfsmolem  7912  fin4i  7940  infpssr  7950  fin1a2lem6  8047  axdc3lem2  8093  axcclem  8099  ttukeylem6  8157  fodomb  8167  gchi  8262  fpwwe2lem5  8272  pwfseqlem4  8300  pwfseq  8302  inawina  8328  wunfi  8359  inar1  8413  ltexnq  8615  ltbtwnnq  8618  ltexprlem4  8679  ltexpri  8683  prlem936  8687  suplem1pr  8692  suplem2pr  8693  recexsrlem  8741  mulgt0sr  8743  map2psrpr  8748  supsr  8750  ledivp1i  9698  nnind  9780  nnmulcl  9785  nnnegz  10043  uzindOLD  10122  ublbneg  10318  xmulasslem  10621  ixxssixx  10686  iccshftri  10786  iccshftli  10788  iccdili  10790  icccntri  10792  seqp1  11077  seqcl2  11080  seqfveq2  11084  seqshft2  11088  monoord  11092  seqsplit  11095  seqcaopr3  11097  seqf1olem2a  11100  seqf1o  11103  seqid2  11108  seqhomo  11109  hashf1lem2  11410  seqcoll  11417  cjre  11640  climeu  12045  climub  12151  fsum2d  12250  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  ruclem9  12532  sadcadd  12665  sadadd2  12667  saddisjlem  12671  smuval2  12689  smupval  12695  smueqlem  12697  smumullem  12699  exprmfct  12805  eulerthlem2  12866  pcmpt  12956  vdwlem10  13053  prmlem1a  13124  mreexexd  13566  letsr  14365  sylow1lem1  14925  efginvrel2  15052  efgsrel  15059  gsum2d  15239  dprdval  15254  ablfac1eulem  15323  pgpfac1  15331  pgpfac  15335  mplcoe1  16225  mplcoe3  16226  mplcoe2  16227  tg2  16719  neindisj2  16876  t1t0  17092  fiuncmp  17147  hmeof1o  17471  ist1-5lem  17527  t1r0  17528  alexsublem  17754  imasdsf1olem  17953  tgioo  18318  fsumcn  18390  voliunlem3  18925  itgfsum  19197  dvbsss  19268  dvmptfsum  19338  dvfsumlem2  19390  dvfsumlem4  19392  mpfaddcl  19442  mpfmulcl  19443  pf1addcl  19452  pf1mulcl  19453  plyco  19639  dgrcolem1  19670  dgrco  19672  dvntaylp  19766  taylthlem1  19768  jensen  20299  bposlem5  20543  lgsquad2lem2  20614  dchrisum0flb  20675  pntpbnd1  20751  pntlemf  20770  opidon2  21007  isexid2  21008  grpomndo  21029  elghomlem2  21045  rngoidmlem  21106  rngoueqz  21113  blocn2  21402  cvexchlem  22964  cdj3lem2b  23033  issgon  23499  subfacp1lem6  23731  cvmliftlem7  23837  cvmliftlem10  23840  eupath2  23919  relexp0  24040  relexpsucr  24041  relexpsucl  24043  relexprel  24046  relexpdm  24047  relexprn  24048  relexpadd  24050  relexpindlem  24051  relexpind  24052  rtrclreclem.trans  24058  rtrclreclem.min  24059  dfrtrcl2  24060  rtrclind  24061  pprodss4v  24495  brbtwn  24599  brcgr  24600  segleantisym  24810  rankeq1o  24873  inpws1  25145  mapmapmap  25251  injsurinj  25252  prl  25270  prl2  25272  sege  25355  mxlmnl2  25373  defse3  25375  dfps2  25392  ablocomgrp  25445  grpodivfo  25477  grpodrcan  25478  grpodlcan  25479  rngodmeqrn  25522  mulinvsca  25583  glmrngo  25585  svs2  25590  truni2  25609  truni3  25610  intopcoaconlem3b  25641  intcont  25646  fil2ss  25660  prdnei  25676  limptlimpr2lem1  25677  islimrs4  25685  bwt2  25695  xrletr2  25721  lvsovso  25729  supnuf  25732  addcanrg  25770  negveud  25771  negveudr  25772  subctct  25957  tartarmap  25991  inttarcar  26004  carinttar  26005  fnctartar  26010  fnctartar2  26011  codcatfun  26037  grphidmor2  26056  cmp2morp  26061  cmp2morpcatt  26065  setiscat  26082  indcls2  26099  clscnc  26113  lineval5a  26191  lineval6a  26192  isconcl6a  26206  isconcl6ab  26207  isibg2aa  26215  isib2g1a1  26219  isibg2a  26221  isibg1a3a  26225  isibg1spa  26226  isibg1a5a  26227  bsstr  26231  nbssntr  26232  lppotoslem  26246  lppotos  26247  nbssntrs  26250  abhp  26276  mettrifi  26576  iscringd  26727  mzpadd  26919  mzpmul  26920  mzpcompact2  26933  dford3lem2  27223  aomclem6  27259  cnsrexpcl  27473  pmtrfrn  27503  ax10ext  27709  iotavalsb  27736  fmul01  27813  fmulcl  27814  fmuldfeqlem1  27815  fmuldfeq  27816  stoweidlem2  27854  stoweidlem3  27855  stoweidlem17  27869  stoweidlem21  27873  stoweidlem26  27878  stoweidlem31  27883  stoweidlem34  27886  stoweidlem48  27900  eu2ndop1stv  28083  funressnfv  28096  afv0fv0  28117  afv0nbfvbi  28119  uslisumgra  28246  usisuslgra  28247  usgra0v  28251  usgra1v  28260  nbusgra  28277  iscusgra0  28293  cusgrauvtx  28309  2mwlk  28330  trliswlk  28338  usgrnloop  28351  pthistrl  28358  spthispth  28359  pthdepisspth  28360  redwlk  28364  wlkdvspth  28366  crctistrl  28373  cyclispth  28374  cycliscrct  28375  cyclnspth  28376  cyclispthon  28378  fargshiftf  28381  fargshiftf1  28382  fargshiftfo  28383  eupatrl  28385  usgrcyclnl1  28386  usgrcyclnl2  28387  nvnencycllem  28389  3v3e3cycl1  28390  constr3trllem5  28400  constr3trl  28405  constr3pth  28406  constr3cycl  28407  4cycl4v4e  28412  4cycl4dv4e  28414  3vfriswmgra  28429  3cyclfrgrarn1  28435  3cyclfrgrarn  28436  n4cyclfrgra  28440  bnj938  29285  bnj964  29291  bnj1052  29321  bnj1125  29338  ax16iNEW7  29526  cdlemk35s  31748  cdlemk39s  31750  cdlemk42  31752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator