MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpcom Structured version   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  2130  ceqex  3058  limomss  4842  elimasni  5223  sotri  5253  sotriOLD  5258  relcoi1  5390  unixpid  5396  f1ocnv  5679  tz6.12c  5742  funbrfv  5757  oprabid  6097  ndmovordi  6230  unielxp  6377  f1o2ndf1  6446  smogt  6621  oawordeulem  6789  omass  6815  ecopovtrn  6999  php  7283  unxpdom  7308  findcard3  7342  isfinite2  7357  cantnfval2  7616  cantnfle  7618  cantnfp1lem3  7628  cantnflem1  7637  cnfcom  7649  rankr1ai  7716  rankonidlem  7746  rankxplim2  7796  oncard  7839  ficardom  7840  cardne  7844  acnnum  7925  alephord2i  7950  cardaleph  7962  aceq3lem  7993  dfac5lem5  8000  dfac12lem3  8017  cdainf  8064  ackbij1lem16  8107  cfslb  8138  cfslb2n  8140  cfsmolem  8142  fin4i  8170  infpssr  8180  fin1a2lem6  8277  axdc3lem2  8323  axcclem  8329  ttukeylem6  8386  fodomb  8396  gchi  8491  fpwwe2lem5  8501  pwfseqlem4  8529  pwfseq  8531  inawina  8557  wunfi  8588  inar1  8642  ltexnq  8844  ltbtwnnq  8847  ltexprlem4  8908  ltexpri  8912  prlem936  8916  suplem1pr  8921  suplem2pr  8922  recexsrlem  8970  mulgt0sr  8972  map2psrpr  8977  supsr  8979  eqlei  9175  eqlei2  9176  ledivp1i  9928  nnind  10010  nnmulcl  10015  nnnegz  10277  uzindOLD  10356  ublbneg  10552  xmulasslem  10856  ixxssixx  10922  iccshftri  11023  iccshftli  11025  iccdili  11027  icccntri  11029  1fv  11112  seqp1  11330  seqcl2  11333  seqfveq2  11337  seqshft2  11341  monoord  11345  seqsplit  11348  seqcaopr3  11350  seqf1olem2a  11353  seqf1o  11356  seqid2  11361  seqhomo  11362  hashf1rn  11628  hashinfxadd  11651  hashle00  11661  hash2pr  11679  hashf1lem2  11697  seqcoll  11704  brfi1uzind  11707  cjre  11936  climeu  12341  climub  12447  fsum2d  12547  fsumabs  12572  fsumrlim  12582  fsumo1  12583  fsumiun  12592  ruclem9  12829  sadcadd  12962  sadadd2  12964  saddisjlem  12968  smuval2  12986  smupval  12992  smueqlem  12994  smumullem  12996  exprmfct  13102  eulerthlem2  13163  pcmpt  13253  vdwlem10  13350  prmlem1a  13421  mreexexd  13865  letsr  14664  sylow1lem1  15224  efginvrel2  15351  efgsrel  15358  gsum2d  15538  dprdval  15553  ablfac1eulem  15622  pgpfac1  15630  pgpfac  15634  mplcoe1  16520  mplcoe3  16521  mplcoe2  16522  tg2  17022  neindisj2  17179  neiptopnei  17188  t1t0  17404  fiuncmp  17459  bwth  17465  hmeof1o  17788  ist1-5lem  17844  t1r0  17845  alexsublem  18067  imasdsf1olem  18395  tgioo  18819  fsumcn  18892  voliunlem3  19438  itgfsum  19710  dvbsss  19781  dvmptfsum  19851  dvfsumlem2  19903  dvfsumlem4  19905  mpfaddcl  19955  mpfmulcl  19956  pf1addcl  19965  pf1mulcl  19966  plyco  20152  dgrcolem1  20183  dgrco  20185  dvntaylp  20279  taylthlem1  20281  jensen  20819  bposlem5  21064  lgsquad2lem2  21135  dchrisum0flb  21196  pntpbnd1  21272  pntlemf  21291  uhgra0v  21337  umisuhgra  21354  uslisumgra  21378  usisuslgra  21379  usgra0v  21383  usgranloopv  21390  usgranloop  21391  usgra1v  21401  usgraidx2vlem2  21403  usgrafisindb0  21414  usgrafisindb1  21415  usgrafisinds  21419  usgrafisbase  21420  iscusgra0  21458  cusgrasize2inds  21478  cusgrafi  21483  2mwlk  21520  trliswlk  21531  2trllemE  21545  usgrnloop  21555  pthistrl  21564  spthispth  21565  pthdepisspth  21566  redwlk  21598  wlkdvspth  21600  crctistrl  21607  cyclispth  21608  cycliscrct  21609  cyclnspth  21610  cyclispthon  21612  fargshiftf  21615  fargshiftf1  21616  fargshiftfo  21617  usgrcyclnl1  21619  usgrcyclnl2  21620  nvnencycllem  21622  3v3e3cycl1  21623  constr3trllem5  21633  constr3trl  21638  constr3pth  21639  constr3cycl  21640  4cycl4v4e  21645  4cycl4dv4e  21647  cusconngra  21655  eupatrl  21682  eupath2  21694  opidon2  21904  isexid2  21905  grpomndo  21926  elghomlem2  21942  rngoidmlem  22003  rngoueqz  22010  blocn2  22301  cvexchlem  23863  cdj3lem2b  23932  issgon  24498  sitgclg  24648  subfacp1lem6  24863  cvmliftlem7  24970  cvmliftlem10  24973  relexp0  25121  relexpsucr  25122  relexpsucl  25124  relexprel  25126  relexpdm  25127  relexprn  25128  relexpadd  25130  relexpindlem  25131  relexpind  25132  rtrclreclem.trans  25138  rtrclreclem.min  25139  dfrtrcl2  25140  rtrclind  25141  prodfn0  25214  prodfrec  25215  ntrivcvg  25217  fprodabs  25289  fprodefsum  25290  fprod2d  25297  pprodss4v  25721  brbtwn  25830  brcgr  25831  segleantisym  26041  rankeq1o  26104  mblfinlem2  26235  mbfresfi  26243  mettrifi  26454  iscringd  26600  mzpadd  26786  mzpmul  26787  mzpcompact2  26800  dford3lem2  27089  aomclem6  27125  cnsrexpcl  27338  pmtrfrn  27368  ax10ext  27574  iotavalsb  27601  fmul01  27677  fmulcl  27678  fmuldfeqlem1  27679  fmuldfeq  27680  stoweidlem2  27718  stoweidlem3  27719  stoweidlem6  27722  stoweidlem8  27724  stoweidlem17  27733  stoweidlem19  27735  stoweidlem21  27737  stoweidlem26  27742  stoweidlem31  27747  stoweidlem43  27759  eu2ndop1stv  27947  funressnfv  27959  afv0fv0  27980  afv0nbfvbi  27982  ssfz12  28088  fzo1fzo0n0  28111  ssfzo12  28113  swrdswrd  28165  swrdccatin12lem3a  28174  swrdccat  28182  swrdccatin1d  28186  swrdccatin2d  28187  swrdccatin12d  28188  2cshw1lem2  28215  cshwssizelem1a  28242  cshwssizelem3  28245  usgra2pthspth  28258  usgra2wlkspth  28261  spthdifv  28262  usgra2pth  28264  usgra2adedgspthlem2  28267  2spontn0vne  28307  usg2spthonot  28308  usg2spthonot0  28309  usgfidegfi  28313  3vfriswmgra  28332  3cyclfrgrarn1  28339  3cyclfrgrarn  28340  n4cyclfrgra  28345  frgranbnb  28347  frconngra  28348  vdfrgra0  28349  vdgfrgra0  28350  vdn0frgrav2  28351  vdgn0frgrav2  28352  frgrancvvdeqlem4  28359  frgrancvvdeqlem7  28362  frgrancvvdeqlemA  28363  frgrancvvdeqlemB  28364  frgrawopreglem2  28371  frgrawopreglem4  28373  frgrawopreglem5  28374  frgrawopreg  28375  frgraregorufr0  28378  frgraeu  28380  frg2wot1  28383  frg2woteqm  28385  frg2woteq  28386  frgregordn0  28396  bnj938  29245  bnj964  29251  bnj1052  29281  bnj1125  29298  ax16iNEW7  29488  cdlemk35s  31671  cdlemk39s  31673  cdlemk42  31675
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator