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  2095  ceqex  3026  limomss  4809  elimasni  5190  sotri  5220  sotriOLD  5225  relcoi1  5357  unixpid  5363  f1ocnv  5646  tz6.12c  5709  funbrfv  5724  oprabid  6064  ndmovordi  6197  unielxp  6344  f1o2ndf1  6413  smogt  6588  oawordeulem  6756  omass  6782  ecopovtrn  6966  php  7250  unxpdom  7275  findcard3  7309  isfinite2  7324  cantnfval2  7580  cantnfle  7582  cantnfp1lem3  7592  cantnflem1  7601  cnfcom  7613  rankr1ai  7680  rankonidlem  7710  rankxplim2  7760  oncard  7803  ficardom  7804  cardne  7808  acnnum  7889  alephord2i  7914  cardaleph  7926  aceq3lem  7957  dfac5lem5  7964  dfac12lem3  7981  cdainf  8028  ackbij1lem16  8071  cfslb  8102  cfslb2n  8104  cfsmolem  8106  fin4i  8134  infpssr  8144  fin1a2lem6  8241  axdc3lem2  8287  axcclem  8293  ttukeylem6  8350  fodomb  8360  gchi  8455  fpwwe2lem5  8465  pwfseqlem4  8493  pwfseq  8495  inawina  8521  wunfi  8552  inar1  8606  ltexnq  8808  ltbtwnnq  8811  ltexprlem4  8872  ltexpri  8876  prlem936  8880  suplem1pr  8885  suplem2pr  8886  recexsrlem  8934  mulgt0sr  8936  map2psrpr  8941  supsr  8943  eqlei  9139  eqlei2  9140  ledivp1i  9892  nnind  9974  nnmulcl  9979  nnnegz  10241  uzindOLD  10320  ublbneg  10516  xmulasslem  10820  ixxssixx  10886  iccshftri  10987  iccshftli  10989  iccdili  10991  icccntri  10993  1fv  11075  seqp1  11293  seqcl2  11296  seqfveq2  11300  seqshft2  11304  monoord  11308  seqsplit  11311  seqcaopr3  11313  seqf1olem2a  11316  seqf1o  11319  seqid2  11324  seqhomo  11325  hashf1rn  11591  hashinfxadd  11614  hashle00  11624  hash2pr  11642  hashf1lem2  11660  seqcoll  11667  brfi1uzind  11670  cjre  11899  climeu  12304  climub  12410  fsum2d  12510  fsumabs  12535  fsumrlim  12545  fsumo1  12546  fsumiun  12555  ruclem9  12792  sadcadd  12925  sadadd2  12927  saddisjlem  12931  smuval2  12949  smupval  12955  smueqlem  12957  smumullem  12959  exprmfct  13065  eulerthlem2  13126  pcmpt  13216  vdwlem10  13313  prmlem1a  13384  mreexexd  13828  letsr  14627  sylow1lem1  15187  efginvrel2  15314  efgsrel  15321  gsum2d  15501  dprdval  15516  ablfac1eulem  15585  pgpfac1  15593  pgpfac  15597  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  tg2  16985  neindisj2  17142  neiptopnei  17151  t1t0  17366  fiuncmp  17421  hmeof1o  17749  ist1-5lem  17805  t1r0  17806  alexsublem  18028  imasdsf1olem  18356  tgioo  18780  fsumcn  18853  voliunlem3  19399  itgfsum  19671  dvbsss  19742  dvmptfsum  19812  dvfsumlem2  19864  dvfsumlem4  19866  mpfaddcl  19916  mpfmulcl  19917  pf1addcl  19926  pf1mulcl  19927  plyco  20113  dgrcolem1  20144  dgrco  20146  dvntaylp  20240  taylthlem1  20242  jensen  20780  bposlem5  21025  lgsquad2lem2  21096  dchrisum0flb  21157  pntpbnd1  21233  pntlemf  21252  uhgra0v  21298  umisuhgra  21315  uslisumgra  21339  usisuslgra  21340  usgra0v  21344  usgranloopv  21351  usgranloop  21352  usgra1v  21362  usgraidx2vlem2  21364  usgrafisindb0  21375  usgrafisindb1  21376  usgrafisinds  21380  usgrafisbase  21381  iscusgra0  21419  cusgrasize2inds  21439  cusgrafi  21444  2mwlk  21481  trliswlk  21492  2trllemE  21506  usgrnloop  21516  pthistrl  21525  spthispth  21526  pthdepisspth  21527  redwlk  21559  wlkdvspth  21561  crctistrl  21568  cyclispth  21569  cycliscrct  21570  cyclnspth  21571  cyclispthon  21573  fargshiftf  21576  fargshiftf1  21577  fargshiftfo  21578  usgrcyclnl1  21580  usgrcyclnl2  21581  nvnencycllem  21583  3v3e3cycl1  21584  constr3trllem5  21594  constr3trl  21599  constr3pth  21600  constr3cycl  21601  4cycl4v4e  21606  4cycl4dv4e  21608  cusconngra  21616  eupatrl  21643  eupath2  21655  opidon2  21865  isexid2  21866  grpomndo  21887  elghomlem2  21903  rngoidmlem  21964  rngoueqz  21971  blocn2  22262  cvexchlem  23824  cdj3lem2b  23893  issgon  24459  sitgclg  24609  subfacp1lem6  24824  cvmliftlem7  24931  cvmliftlem10  24934  relexp0  25082  relexpsucr  25083  relexpsucl  25085  relexprel  25087  relexpdm  25088  relexprn  25089  relexpadd  25091  relexpindlem  25092  relexpind  25093  rtrclreclem.trans  25099  rtrclreclem.min  25100  dfrtrcl2  25101  rtrclind  25102  prodfn0  25175  prodfrec  25176  ntrivcvg  25178  fprodabs  25250  fprodefsum  25251  fprod2d  25258  pprodss4v  25638  brbtwn  25742  brcgr  25743  segleantisym  25953  rankeq1o  26016  mblfinlem2  26144  mbfresfi  26152  mettrifi  26353  iscringd  26499  mzpadd  26685  mzpmul  26686  mzpcompact2  26699  dford3lem2  26988  aomclem6  27024  cnsrexpcl  27238  pmtrfrn  27268  ax10ext  27474  iotavalsb  27501  fmul01  27577  fmulcl  27578  fmuldfeqlem1  27579  fmuldfeq  27580  stoweidlem2  27618  stoweidlem3  27619  stoweidlem6  27622  stoweidlem8  27624  stoweidlem17  27633  stoweidlem19  27635  stoweidlem21  27637  stoweidlem26  27642  stoweidlem31  27647  stoweidlem43  27659  eu2ndop1stv  27847  funressnfv  27859  afv0fv0  27880  afv0nbfvbi  27882  ssfz12  27976  fzo1fzo0n0  27988  ssfzo12  27990  swrdswrd  28011  swrdccatin12lem3a  28021  swrdccatin12b  28027  usgra2pthspth  28035  usgra2wlkspth  28038  spthdifv  28039  usgra2pth  28041  usgra2adedgspthlem2  28044  2spontn0vne  28084  usg2spthonot  28085  usg2spthonot0  28086  usgfidegfi  28090  3vfriswmgra  28109  3cyclfrgrarn1  28116  3cyclfrgrarn  28117  n4cyclfrgra  28122  frgranbnb  28124  frconngra  28125  vdfrgra0  28126  vdgfrgra0  28127  vdn0frgrav2  28128  vdgn0frgrav2  28129  frgrancvvdeqlem4  28136  frgrancvvdeqlem7  28139  frgrancvvdeqlemA  28140  frgrancvvdeqlemB  28141  frgrawopreglem2  28148  frgrawopreglem4  28150  frgrawopreglem5  28151  frgrawopreg  28152  frgraregorufr0  28155  frgraeu  28157  frg2wot1  28160  frg2woteqm  28162  frg2woteq  28163  frgregordn0  28173  bnj938  29014  bnj964  29020  bnj1052  29050  bnj1125  29067  ax16iNEW7  29255  cdlemk35s  31419  cdlemk39s  31421  cdlemk42  31423
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator