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  2079  ceqex  3009  limomss  4790  elimasni  5171  sotri  5201  sotriOLD  5206  relcoi1  5338  unixpid  5344  f1ocnv  5627  tz6.12c  5690  funbrfv  5704  oprabid  6044  ndmovordi  6177  unielxp  6324  smogt  6565  oawordeulem  6733  omass  6759  ecopovtrn  6943  php  7227  unxpdom  7252  findcard3  7286  isfinite2  7301  cantnfval2  7557  cantnfle  7559  cantnfp1lem3  7569  cantnflem1  7578  cnfcom  7590  rankr1ai  7657  rankonidlem  7687  rankxplim2  7737  oncard  7780  ficardom  7781  cardne  7785  acnnum  7866  alephord2i  7891  cardaleph  7903  aceq3lem  7934  dfac5lem5  7941  dfac12lem3  7958  cdainf  8005  ackbij1lem16  8048  cfslb  8079  cfslb2n  8081  cfsmolem  8083  fin4i  8111  infpssr  8121  fin1a2lem6  8218  axdc3lem2  8264  axcclem  8270  ttukeylem6  8327  fodomb  8337  gchi  8432  fpwwe2lem5  8442  pwfseqlem4  8470  pwfseq  8472  inawina  8498  wunfi  8529  inar1  8583  ltexnq  8785  ltbtwnnq  8788  ltexprlem4  8849  ltexpri  8853  prlem936  8857  suplem1pr  8862  suplem2pr  8863  recexsrlem  8911  mulgt0sr  8913  map2psrpr  8918  supsr  8920  ledivp1i  9868  nnind  9950  nnmulcl  9955  nnnegz  10217  uzindOLD  10296  ublbneg  10492  xmulasslem  10796  ixxssixx  10862  iccshftri  10963  iccshftli  10965  iccdili  10967  icccntri  10969  1fv  11050  seqp1  11265  seqcl2  11268  seqfveq2  11272  seqshft2  11276  monoord  11280  seqsplit  11283  seqcaopr3  11285  seqf1olem2a  11288  seqf1o  11291  seqid2  11296  seqhomo  11297  hashinfxadd  11586  hashle00  11596  hash2pr  11614  hashf1lem2  11632  seqcoll  11639  brfi1uzind  11642  cjre  11871  climeu  12276  climub  12382  fsum2d  12482  fsumabs  12507  fsumrlim  12517  fsumo1  12518  fsumiun  12527  ruclem9  12764  sadcadd  12897  sadadd2  12899  saddisjlem  12903  smuval2  12921  smupval  12927  smueqlem  12929  smumullem  12931  exprmfct  13037  eulerthlem2  13098  pcmpt  13188  vdwlem10  13285  prmlem1a  13356  mreexexd  13800  letsr  14599  sylow1lem1  15159  efginvrel2  15286  efgsrel  15293  gsum2d  15473  dprdval  15488  ablfac1eulem  15557  pgpfac1  15565  pgpfac  15569  mplcoe1  16455  mplcoe3  16456  mplcoe2  16457  tg2  16953  neindisj2  17110  neiptopnei  17119  t1t0  17334  fiuncmp  17389  hmeof1o  17717  ist1-5lem  17773  t1r0  17774  alexsublem  17996  imasdsf1olem  18311  tgioo  18698  fsumcn  18771  voliunlem3  19313  itgfsum  19585  dvbsss  19656  dvmptfsum  19726  dvfsumlem2  19778  dvfsumlem4  19780  mpfaddcl  19830  mpfmulcl  19831  pf1addcl  19840  pf1mulcl  19841  plyco  20027  dgrcolem1  20058  dgrco  20060  dvntaylp  20154  taylthlem1  20156  jensen  20694  bposlem5  20939  lgsquad2lem2  21010  dchrisum0flb  21071  pntpbnd1  21147  pntlemf  21166  uhgra0v  21212  umisuhgra  21229  uslisumgra  21253  usisuslgra  21254  usgra0v  21258  usgra1v  21275  usgraidx2vlem2  21277  usgrafisindb0  21288  usgrafisindb1  21289  usgrafisinds  21293  usgrafisbase  21294  nbusgra  21306  iscusgra0  21332  cusgrasize2inds  21352  cusgrafi  21357  2mwlk  21392  trliswlk  21403  usgrnloop  21419  pthistrl  21426  spthispth  21427  pthdepisspth  21428  constr2trl  21446  redwlk  21454  wlkdvspth  21456  crctistrl  21463  cyclispth  21464  cycliscrct  21465  cyclnspth  21466  cyclispthon  21468  fargshiftf  21471  fargshiftf1  21472  fargshiftfo  21473  usgrcyclnl1  21475  usgrcyclnl2  21476  nvnencycllem  21478  3v3e3cycl1  21479  constr3trllem5  21489  constr3trl  21494  constr3pth  21495  constr3cycl  21496  4cycl4v4e  21501  4cycl4dv4e  21503  cusconngra  21511  eupatrl  21538  eupath2  21550  opidon2  21760  isexid2  21761  grpomndo  21782  elghomlem2  21798  rngoidmlem  21859  rngoueqz  21866  blocn2  22157  cvexchlem  23719  cdj3lem2b  23788  issgon  24302  subfacp1lem6  24650  cvmliftlem7  24757  cvmliftlem10  24760  relexp0  24908  relexpsucr  24909  relexpsucl  24911  relexprel  24913  relexpdm  24914  relexprn  24915  relexpadd  24917  relexpindlem  24918  relexpind  24919  rtrclreclem.trans  24925  rtrclreclem.min  24926  dfrtrcl2  24927  rtrclind  24928  prodfn0  25001  prodfrec  25002  ntrivcvg  25004  fprodabs  25076  fprodefsum  25077  pprodss4v  25448  brbtwn  25552  brcgr  25553  segleantisym  25763  rankeq1o  25826  mettrifi  26154  iscringd  26300  mzpadd  26486  mzpmul  26487  mzpcompact2  26500  dford3lem2  26789  aomclem6  26825  cnsrexpcl  27039  pmtrfrn  27069  ax10ext  27275  iotavalsb  27302  fmul01  27378  fmulcl  27379  fmuldfeqlem1  27380  fmuldfeq  27381  stoweidlem2  27419  stoweidlem3  27420  stoweidlem6  27423  stoweidlem8  27425  stoweidlem17  27434  stoweidlem19  27436  stoweidlem21  27438  stoweidlem26  27443  stoweidlem31  27448  stoweidlem43  27460  eu2ndop1stv  27648  funressnfv  27661  afv0fv0  27682  afv0nbfvbi  27684  3vfriswmgra  27758  3cyclfrgrarn1  27765  3cyclfrgrarn  27766  n4cyclfrgra  27771  frgranbnb  27773  frconngra  27774  vdfrgra0  27775  vdgfrgra0  27776  vdn0frgrav2  27777  vdgn0frgrav2  27778  frgrancvvdeqlem4  27785  frgrancvvdeqlem7  27788  frgrancvvdeqlemA  27789  frgrancvvdeqlemB  27790  frgrawopreglem2  27797  frgrawopreglem4  27799  frgrawopreglem5  27800  frgrawopreg  27801  frgraregorufr0  27804  bnj938  28646  bnj964  28652  bnj1052  28682  bnj1125  28699  ax16iNEW7  28887  cdlemk35s  31051  cdlemk39s  31053  cdlemk42  31055
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator