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

Theorem mpcom 34
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 29 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
41, 3mpd 15 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syldan  457  ax16i  2072  ceqex  3002  limomss  4783  elimasni  5164  sotri  5194  sotriOLD  5199  relcoi1  5331  unixpid  5337  f1ocnv  5620  tz6.12c  5683  funbrfv  5697  oprabid  6037  ndmovordi  6170  unielxp  6317  smogt  6558  oawordeulem  6726  omass  6752  ecopovtrn  6936  php  7220  unxpdom  7245  findcard3  7279  isfinite2  7294  cantnfval2  7550  cantnfle  7552  cantnfp1lem3  7562  cantnflem1  7571  cnfcom  7583  rankr1ai  7650  rankonidlem  7680  rankxplim2  7730  oncard  7773  ficardom  7774  cardne  7778  acnnum  7859  alephord2i  7884  cardaleph  7896  aceq3lem  7927  dfac5lem5  7934  dfac12lem3  7951  cdainf  7998  ackbij1lem16  8041  cfslb  8072  cfslb2n  8074  cfsmolem  8076  fin4i  8104  infpssr  8114  fin1a2lem6  8211  axdc3lem2  8257  axcclem  8263  ttukeylem6  8320  fodomb  8330  gchi  8425  fpwwe2lem5  8435  pwfseqlem4  8463  pwfseq  8465  inawina  8491  wunfi  8522  inar1  8576  ltexnq  8778  ltbtwnnq  8781  ltexprlem4  8842  ltexpri  8846  prlem936  8850  suplem1pr  8855  suplem2pr  8856  recexsrlem  8904  mulgt0sr  8906  map2psrpr  8911  supsr  8913  ledivp1i  9861  nnind  9943  nnmulcl  9948  nnnegz  10210  uzindOLD  10289  ublbneg  10485  xmulasslem  10789  ixxssixx  10855  iccshftri  10956  iccshftli  10958  iccdili  10960  icccntri  10962  1fv  11043  seqp1  11258  seqcl2  11261  seqfveq2  11265  seqshft2  11269  monoord  11273  seqsplit  11276  seqcaopr3  11278  seqf1olem2a  11281  seqf1o  11284  seqid2  11289  seqhomo  11290  hashinfxadd  11579  hashle00  11589  hash2pr  11607  hashf1lem2  11625  seqcoll  11632  brfi1uzind  11635  cjre  11864  climeu  12269  climub  12375  fsum2d  12475  fsumabs  12500  fsumrlim  12510  fsumo1  12511  fsumiun  12520  ruclem9  12757  sadcadd  12890  sadadd2  12892  saddisjlem  12896  smuval2  12914  smupval  12920  smueqlem  12922  smumullem  12924  exprmfct  13030  eulerthlem2  13091  pcmpt  13181  vdwlem10  13278  prmlem1a  13349  mreexexd  13793  letsr  14592  sylow1lem1  15152  efginvrel2  15279  efgsrel  15286  gsum2d  15466  dprdval  15481  ablfac1eulem  15550  pgpfac1  15558  pgpfac  15562  mplcoe1  16448  mplcoe3  16449  mplcoe2  16450  tg2  16946  neindisj2  17103  neiptopnei  17112  t1t0  17327  fiuncmp  17382  hmeof1o  17710  ist1-5lem  17766  t1r0  17767  alexsublem  17989  imasdsf1olem  18304  tgioo  18691  fsumcn  18764  voliunlem3  19306  itgfsum  19578  dvbsss  19649  dvmptfsum  19719  dvfsumlem2  19771  dvfsumlem4  19773  mpfaddcl  19823  mpfmulcl  19824  pf1addcl  19833  pf1mulcl  19834  plyco  20020  dgrcolem1  20051  dgrco  20053  dvntaylp  20147  taylthlem1  20149  jensen  20687  bposlem5  20932  lgsquad2lem2  21003  dchrisum0flb  21064  pntpbnd1  21140  pntlemf  21159  uhgra0v  21205  umisuhgra  21222  uslisumgra  21246  usisuslgra  21247  usgra0v  21251  usgra1v  21268  usgraidx2vlem2  21270  usgrafisindb0  21281  usgrafisindb1  21282  usgrafisinds  21286  usgrafisbase  21287  nbusgra  21299  iscusgra0  21325  cusgrasize2inds  21345  cusgrafi  21350  2mwlk  21385  trliswlk  21396  usgrnloop  21412  pthistrl  21419  spthispth  21420  pthdepisspth  21421  constr2trl  21439  redwlk  21447  wlkdvspth  21449  crctistrl  21456  cyclispth  21457  cycliscrct  21458  cyclnspth  21459  cyclispthon  21461  fargshiftf  21464  fargshiftf1  21465  fargshiftfo  21466  usgrcyclnl1  21468  usgrcyclnl2  21469  nvnencycllem  21471  3v3e3cycl1  21472  constr3trllem5  21482  constr3trl  21487  constr3pth  21488  constr3cycl  21489  4cycl4v4e  21494  4cycl4dv4e  21496  cusconngra  21504  eupatrl  21531  eupath2  21543  opidon2  21753  isexid2  21754  grpomndo  21775  elghomlem2  21791  rngoidmlem  21852  rngoueqz  21859  blocn2  22150  cvexchlem  23712  cdj3lem2b  23781  issgon  24295  subfacp1lem6  24643  cvmliftlem7  24750  cvmliftlem10  24753  relexp0  24901  relexpsucr  24902  relexpsucl  24904  relexprel  24906  relexpdm  24907  relexprn  24908  relexpadd  24910  relexpindlem  24911  relexpind  24912  rtrclreclem.trans  24918  rtrclreclem.min  24919  dfrtrcl2  24920  rtrclind  24921  prodfn0  24994  prodfrec  24995  ntrivcvg  24997  fprodabs  25069  fprodefsum  25070  pprodss4v  25441  brbtwn  25545  brcgr  25546  segleantisym  25756  rankeq1o  25819  mettrifi  26147  iscringd  26293  mzpadd  26479  mzpmul  26480  mzpcompact2  26493  dford3lem2  26782  aomclem6  26818  cnsrexpcl  27032  pmtrfrn  27062  ax10ext  27268  iotavalsb  27295  fmul01  27371  fmulcl  27372  fmuldfeqlem1  27373  fmuldfeq  27374  stoweidlem2  27412  stoweidlem3  27413  stoweidlem6  27416  stoweidlem8  27418  stoweidlem17  27427  stoweidlem19  27429  stoweidlem21  27431  stoweidlem26  27436  stoweidlem31  27441  stoweidlem43  27453  eu2ndop1stv  27641  funressnfv  27654  afv0fv0  27675  afv0nbfvbi  27677  3vfriswmgra  27751  3cyclfrgrarn1  27758  3cyclfrgrarn  27759  n4cyclfrgra  27764  frgranbnb  27766  frconngra  27767  vdfrgra0  27768  vdgfrgra0  27769  vdn0frgrav2  27770  vdgn0frgrav2  27771  frgrancvvdeqlem4  27778  frgrancvvdeqlem7  27781  frgrancvvdeqlemA  27782  frgrancvvdeqlemB  27783  frgrawopreglem2  27790  frgrawopreglem4  27792  frgrawopreglem5  27793  frgrawopreg  27794  frgraregorufr0  27797  bnj938  28639  bnj964  28645  bnj1052  28675  bnj1125  28692  ax16iNEW7  28880  cdlemk35s  31102  cdlemk39s  31104  cdlemk42  31106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator