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

Theorem mpcom 37
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 32 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
41, 3mpd 15 1  |-  ( ps 
->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syldan  477  axc16i  2167  sbcn1  3325  sbcim1  3326  sbcbi1  3327  sbcel21v  3340  elimasni  5214  sotri  5246  relcoi1OLD  5384  unixpid  5390  f0rn0  5791  f1ocnv  5849  tz6.12c  5907  funbrfv  5926  f1dom3el3dif  6194  oprabid  6342  oprabv  6366  ndmovordi  6487  elovmpt2rab  6542  elovmpt2rab1  6543  elovmpt3rab1  6554  limomss  6724  unielxp  6856  bropfvvvvlem  6902  f1o2ndf1  6931  smogt  7112  tfrlem1  7120  oawordeulem  7281  omass  7307  ecopovtrn  7492  php  7782  unxpdom  7805  findcard2d  7839  findcard3  7840  isfinite2  7855  fsuppimp  7915  fsuppunfi  7929  fsuppunbi  7930  fsuppres  7934  cantnfval2  8200  cantnfle  8202  cantnfp1lem3  8211  cantnflem1  8220  cnfcom  8231  rankr1ai  8295  rankonidlem  8325  rankxplim2  8377  oncard  8420  ficardom  8421  cardne  8425  acnnum  8509  alephord2i  8534  cardaleph  8546  aceq3lem  8577  dfac5lem5  8584  dfac12lem3  8601  cdainf  8648  ackbij1lem16  8691  cfslb  8722  cfslb2n  8724  cfsmolem  8726  fin4i  8754  infpssr  8764  fin1a2lem6  8861  axdc3lem2  8907  axcclem  8913  ttukeylem6  8970  fodomb  8980  gchi  9075  fpwwe2lem5  9085  pwfseqlem4  9113  pwfseq  9115  inawina  9141  wunfi  9172  inar1  9226  ltexnq  9426  ltbtwnnq  9429  ltexprlem4  9490  ltexpri  9494  prlem936  9498  suplem1pr  9503  suplem2pr  9504  recexsrlem  9553  mulgt0sr  9555  map2psrpr  9560  supsr  9562  eqlei  9770  eqlei2  9771  ledivp1i  10560  nnind  10655  nnmulcl  10660  nn0ge2m1nn  10963  nnnegz  10969  ublbneg  11277  xmulasslem  11600  ixxssixx  11678  iccshftri  11796  iccshftli  11798  iccdili  11800  icccntri  11802  1fv  11939  fzo1fzo0n0  11988  elfzonlteqm1  12020  ssfzo12  12035  zmodidfzoimp  12159  mptnn0fsuppr  12243  seqp1  12260  seqcl2  12263  seqfveq2  12267  seqshft2  12271  monoord  12275  seqsplit  12278  seqcaopr3  12280  seqf1olem2a  12283  seqf1o  12286  seqid2  12291  seqhomo  12292  hashf1rn  12567  hashinfxadd  12596  hashle00  12609  hashf1lem2  12652  seqcoll  12660  hash2pr  12663  pr2pwpr  12669  hashge2el2difr  12671  hash3tr  12680  fi1uzind  12683  brfi1indALT  12686  snopiswrd  12714  elovmptnn0wrd  12746  swrdswrd  12853  swrdccatin12lem2a  12878  swrdccat  12886  swrdccatin1d  12892  swrdccatin2d  12893  swrdccatin12d  12894  repswccat  12925  cshwidxmod  12942  relexpsucnnr  13137  rtrclreclem3  13172  rtrclreclem4  13173  dfrtrcl2  13174  relexpindlem  13175  relexpind  13176  rtrclind  13177  cjre  13251  climeu  13668  climub  13774  fsum2d  13881  fsumabs  13910  fsumrlim  13920  fsumo1  13921  fsumiun  13930  prodfn0  13999  prodfrec  14000  ntrivcvg  14002  fprodabs  14077  fprod2d  14084  fprodefsum  14198  ruclem9  14339  sadcadd  14481  sadadd2  14483  saddisjlem  14487  smuval2  14505  smupval  14511  smueqlem  14513  smumullem  14515  lcmgcdlem  14620  lcmftp  14658  exprmfct  14697  eulerthlem2  14779  pcmpt  14886  vdwlem10  14989  cshwsidrepsw  15113  cshwshashlem1  15115  prmlem1a  15127  ressval3d  15235  mreexexd  15603  letsr  16522  pmtrfrn  17148  pmtr3ncom  17165  gsmtrcl  17206  psgnsn  17210  sylow1lem1  17299  efginvrel2  17426  efgsrel  17433  cntzcmnss  17530  gsumzoppg  17626  gsum2dlem2  17652  telgsumfzs  17668  dprdval  17684  ablfac1eulem  17754  pgpfac1  17762  pgpfac  17766  srgpcomp  17814  ring1ne0  17870  rimf1o  18011  rimrhm  18012  brric2  18022  0ringnnzr  18542  mplcoe1  18738  mplcoe3  18739  mplcoe5lem  18740  mplcoe5  18741  mpfaddcl  18806  mpfmulcl  18807  coe1ae0  18858  coe1fzgsumd  18945  gsummoncoe1  18947  pf1addcl  18990  pf1mulcl  18991  evl1gsumd  18994  zrhpsgnelbas  19211  psgndiflemA  19218  mamufacex  19463  mat0dimcrng  19544  mavmulsolcl  19625  mdetunilem9  19694  cramerlem3  19763  pmatcollpw3fi1  19861  pm2mpfo  19887  chmaidscmat  19921  chfacfscmul0  19931  chfacfpmmul0  19935  cpmadugsumlemF  19949  tg2  20029  neindisj2  20188  neiptopnei  20197  t1t0  20413  fiuncmp  20468  hmeof1o  20828  ist1-5lem  20884  t1r0  20885  alexsublem  21108  imasdsf1olem  21437  tgioo  21863  fsumcn  21951  voliunlem3  22554  itgfsum  22833  dvbsss  22906  dvmptfsum  22976  dvfsumlem2  23028  dvfsumlem4  23030  plyco  23244  dgrcolem1  23276  dgrco  23278  dvntaylp  23375  taylthlem1  23377  jensen  23963  bposlem5  24265  lgsquad2lem2  24336  dchrisum0flb  24397  pntpbnd1  24473  pntlemf  24492  brbtwn  24978  brcgr  24979  ushgrauhgra  25079  uhgra0v  25086  umisuhgra  25103  usgrac  25127  uslgraf1oedg  25135  uslisushgra  25139  uslisumgra  25140  usisuslgra  25141  elusuhgra  25144  usgra0v  25147  usgranloopv  25154  usgranloop  25155  usgra1v  25166  usgraidx2vlem2  25168  usgrafisindb0  25185  usgrafisindb1  25186  usgrafisinds  25190  usgrafisbase  25191  iscusgra0  25234  cusgrasize2inds  25254  cusgrafi  25259  2mwlk  25298  iswlkg  25301  wlkcpr  25306  edgwlk  25308  trliswlk  25318  2trllemE  25332  usgrwlknloop  25342  pthistrl  25351  spthispth  25352  pthdepisspth  25353  redwlk  25385  wlkdvspth  25387  usgra2adedgspthlem2  25389  usgra2wlkspth  25398  crctistrl  25405  cyclispth  25406  cycliscrct  25407  cyclnspth  25408  cyclispthon  25410  fargshiftf  25413  fargshiftf1  25414  fargshiftfo  25415  usgrcyclnl1  25417  usgrcyclnl2  25418  nvnencycllem  25420  3v3e3cycl1  25421  constr3trllem5  25431  constr3trl  25436  constr3pth  25437  constr3cycl  25438  4cycl4v4e  25443  4cycl4dv4e  25445  cusconngra  25453  wwlknimp  25464  wwlkn0  25466  wlkiswwlk1  25467  wlkiswwlk2lem4  25471  wlkiswwlk2  25474  wlklniswwlkn2  25477  wwlkiswwlkn  25479  2wlkeq  25484  wwlknred  25500  wwlknext  25501  wwlknextbi  25502  wwlknredwwlkn0  25504  wwlkextwrd  25505  wwlkm1edg  25512  wwlkextproplem3  25520  isclwlkg  25532  clwlkswlks  25535  clwwlkprop  25547  clwwlkgt0  25548  clwwlknimp  25553  clwlkisclwwlklem2a  25562  clwlkisclwwlklem1  25564  clwwlkext2edg  25579  clwwisshclww  25584  clwwnisshclwwn  25586  usghashecclwwlk  25612  wlklenvclwlk  25616  2spontn0vne  25664  usg2spthonot  25665  usg2spthonot0  25666  usgfidegfi  25687  usgravd00  25696  rgraprop  25705  rusgraprop  25706  rusgrargra  25707  cusgraisrusgra  25715  0eusgraiff0rgracl  25718  rusgrasn  25722  rusgranumwlklem1  25726  eupatrl  25745  eupath2  25757  3vfriswmgra  25782  3cyclfrgrarn1  25789  3cyclfrgrarn  25790  n4cyclfrgra  25795  frgranbnb  25797  frconngra  25798  vdfrgra0  25799  vdn0frgrav2  25800  vdgn0frgrav2  25801  usgn0fidegnn0  25806  frgrancvvdeqlem4  25810  frgrancvvdeqlem7  25813  frgrancvvdeqlemA  25814  frgrancvvdeqlemB  25815  frgrawopreglem4  25824  frgrawopreglem5  25825  frgrawopreg  25826  frgraregorufr0  25829  frgraeu  25831  frg2wot1  25834  frg2woteqm  25836  frg2woteq  25837  frgregordn0  25847  numclwwlkun  25856  numclwwlk8  25892  frgrareggt1  25893  frgrareg  25894  frgraregord013  25895  frgraregord13  25896  frgraogt3nreg  25897  friendshipgt3  25898  friendship  25899  opidon2OLD  26101  isexid2  26102  grpomndo  26123  elghomlem2OLD  26139  rngoidmlem  26200  rngoueqz  26207  blocn2  26498  cvexchlem  28070  cdj3lem2b  28139  cnvoprab  28357  nnindf  28431  issgon  28994  sitgclg  29224  sseqp1  29277  bnj938  29797  bnj964  29803  bnj1052  29833  bnj1125  29850  subfacp1lem6  29957  cvmliftlem7  30063  cvmliftlem10  30066  mclsrcl  30248  pprodss4v  30700  segleantisym  30931  rankeq1o  30987  iooelexlt  31810  relowlssretop  31811  rdgeqoa  31818  poimirlem22  32007  poimirlem25  32010  poimirlem28  32013  poimirlem31  32016  mblfinlem3  32024  mbfresfi  32032  mettrifi  32131  iscringd  32277  cdlemk35s  34549  cdlemk39s  34551  cdlemk42  34553  mzpadd  35625  mzpmul  35626  mzpcompact2  35639  dford3lem2  35927  aomclem6  35962  cnsrexpcl  36076  relexpss1d  36342  iunrelexpmin1  36345  iunrelexpmin2  36349  nzin  36711  axc11next  36801  iotavalsb  36828  fperiodmullem  37559  fmul01  37696  fmulcl  37697  fmuldfeqlem1  37698  fmuldfeq  37699  iblspltprt  37888  itgspltprt  37894  stoweidlem2  37900  stoweidlem3  37901  stoweidlem6  37904  stoweidlem8  37906  stoweidlem17  37915  stoweidlem19  37917  stoweidlem21  37919  stoweidlem26  37924  stoweidlem31  37930  stoweidlem43  37942  fourierdlem42  38050  fourierdlem42OLD  38051  eu2ndop1stv  38661  funressnfv  38667  afv0fv0  38689  afv0nbfvbi  38691  smonoord  38756  mod2eq1n2dvds  38763  iccpartiltu  38774  iccpartigtl  38775  iccelpart  38785  icceuelpart  38788  bgoldbwt  38916  bgoldbtbndlem2  38939  bgoldbtbndlem4  38941  tgoldbach  38949  funopsn  39060  ssfz12  39096  fzoopth  39105  elfzr  39109  elfzo0l  39110  elfzlmr  39111  umgrnloopv  39242  umgrnloop  39244  uspgrf1oedg  39308  usgrnloopvALT  39332  usgrnloopALT  39334  usgredg2vlem2  39353  subgrprop  39395  uvtxaisvtx  39511  vtxnbuvtx  39513  uvtxanbgrvtx  39515  cusgrsize2inds  39564  rgrprop  39628  rusgrprop  39630  2m1wlk  39681  1wlkvtxiedg  39687  1wlk1walk  39697  wlk1wlk  39699  red1wlk  39717  1wlkvtxeledg  39721  lfgr1wlknloop  39724  trlis1wlk  39739  PthisTrl  39759  sPthisPth  39760  pthdivtx  39762  2pthnloop  39764  spthdep  39766  pthdepissPth  39767  isclWlkb  39800  clwlkis1wlk  39801  clwlk1wlk  39802  clWlkcompim  39806  crctprop  39815  cyclprop  39816  crctisclwlk  39817  cyclisCrct  39821  cyclnsPth  39822  cyclisPthon  39823  uspgrn2crct  39826  1pthond  39859  upgr3v3e3cycl  39921  upgr4cycl4dv4e  39926  usgra2pthspth  39938  spthdifv  39939  usgra2pth  39941  uhgrasiz  39979  usgfis  40031  usgfisALT  40035  clcllaw  40100  intop  40112  clintop  40117  assintop  40118  assintopcllaw  40121  lmod0rng  40141  ringrng  40152  rngimf1o  40178  rngimrnghm  40179  ztprmneprm  40401  scmsuppss  40430  ply1mulgsumlem1  40451  ply1mulgsumlem2  40452  lcoel0  40494  ellcoellss  40501  lindslinindsimp2lem5  40528  ldepspr  40539  nno  40601  nn0o  40602  flnn0div2ge  40613  nnolog2flm1  40674  blengt1fldiv2p1  40677  dignn0flhalf  40702
  Copyright terms: Public domain W3C validator