MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpcom Structured 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  472  axc16i  2125  sbcn1  3283  sbcim1  3284  sbcbi1  3285  sbcel21v  3298  elimasni  5152  sotri  5184  relcoi1OLD  5322  unixpid  5328  f0rn0  5723  f1ocnv  5781  tz6.12c  5839  funbrfv  5858  f1dom3el3dif  6123  oprabid  6271  oprabv  6292  ndmovordi  6413  elovmpt2rab  6468  elovmpt2rab1  6469  elovmpt3rab1  6480  limomss  6650  unielxp  6782  f1o2ndf1  6854  smogt  7036  tfrlem1  7044  oawordeulem  7205  omass  7231  ecopovtrn  7416  php  7704  unxpdom  7727  findcard2d  7761  findcard3  7762  isfinite2  7777  fsuppimp  7837  fsuppunfi  7851  fsuppunbi  7852  fsuppres  7856  cantnfval2  8121  cantnfle  8123  cantnfp1lem3  8132  cantnflem1  8141  cnfcom  8152  rankr1ai  8216  rankonidlem  8246  rankxplim2  8298  oncard  8341  ficardom  8342  cardne  8346  acnnum  8429  alephord2i  8454  cardaleph  8466  aceq3lem  8497  dfac5lem5  8504  dfac12lem3  8521  cdainf  8568  ackbij1lem16  8611  cfslb  8642  cfslb2n  8644  cfsmolem  8646  fin4i  8674  infpssr  8684  fin1a2lem6  8781  axdc3lem2  8827  axcclem  8833  ttukeylem6  8890  fodomb  8900  gchi  8995  fpwwe2lem5  9005  pwfseqlem4  9033  pwfseq  9035  inawina  9061  wunfi  9092  inar1  9146  ltexnq  9346  ltbtwnnq  9349  ltexprlem4  9410  ltexpri  9414  prlem936  9418  suplem1pr  9423  suplem2pr  9424  recexsrlem  9473  mulgt0sr  9475  map2psrpr  9480  supsr  9482  eqlei  9690  eqlei2  9691  ledivp1i  10478  nnind  10573  nnmulcl  10578  nn0ge2m1nn  10880  nnnegz  10886  ublbneg  11194  xmulasslem  11517  ixxssixx  11595  iccshftri  11713  iccshftli  11715  iccdili  11717  icccntri  11719  1fv  11854  fzo1fzo0n0  11903  elfzonlteqm1  11934  ssfzo12  11949  zmodidfzoimp  12072  mptnn0fsuppr  12156  seqp1  12173  seqcl2  12176  seqfveq2  12180  seqshft2  12184  monoord  12188  seqsplit  12191  seqcaopr3  12193  seqf1olem2a  12196  seqf1o  12199  seqid2  12204  seqhomo  12205  hashf1rn  12480  hashinfxadd  12509  hashle00  12522  hashf1lem2  12562  seqcoll  12570  hash2pr  12573  pr2pwpr  12579  hashge2el2difr  12581  hash3tr  12590  fi1uzind  12593  brfi1indALT  12596  snopiswrd  12624  elovmptnn0wrd  12653  swrdswrd  12757  swrdccatin12lem2a  12782  swrdccat  12790  swrdccatin1d  12796  swrdccatin2d  12797  swrdccatin12d  12798  repswccat  12829  cshwidxmod  12846  relexpsucnnr  13027  rtrclreclem3  13062  rtrclreclem4  13063  dfrtrcl2  13064  relexpindlem  13065  relexpind  13066  rtrclind  13067  cjre  13141  climeu  13557  climub  13663  fsum2d  13770  fsumabs  13799  fsumrlim  13809  fsumo1  13810  fsumiun  13819  prodfn0  13888  prodfrec  13889  ntrivcvg  13891  fprodabs  13966  fprod2d  13973  fprodefsum  14087  ruclem9  14228  sadcadd  14370  sadadd2  14372  saddisjlem  14376  smuval2  14394  smupval  14400  smueqlem  14402  smumullem  14404  lcmgcdlem  14509  lcmftp  14547  exprmfct  14586  eulerthlem2  14668  pcmpt  14775  vdwlem10  14878  cshwsidrepsw  15002  cshwshashlem1  15004  prmlem1a  15016  ressval3d  15124  mreexexd  15492  letsr  16411  pmtrfrn  17037  pmtr3ncom  17054  gsmtrcl  17095  psgnsn  17099  sylow1lem1  17188  efginvrel2  17315  efgsrel  17322  cntzcmnss  17419  gsumzoppg  17515  gsum2dlem2  17541  telgsumfzs  17557  dprdval  17573  ablfac1eulem  17643  pgpfac1  17651  pgpfac  17655  srgpcomp  17703  ring1ne0  17759  rimf1o  17900  rimrhm  17901  brric2  17911  0ringnnzr  18431  mplcoe1  18627  mplcoe3  18628  mplcoe5lem  18629  mplcoe5  18630  mpfaddcl  18695  mpfmulcl  18696  coe1ae0  18747  coe1fzgsumd  18834  gsummoncoe1  18836  pf1addcl  18879  pf1mulcl  18880  evl1gsumd  18883  zrhpsgnelbas  19099  psgndiflemA  19106  mamufacex  19351  mat0dimcrng  19432  mavmulsolcl  19513  mdetunilem9  19582  cramerlem3  19651  pmatcollpw3fi1  19749  pm2mpfo  19775  chmaidscmat  19809  chfacfscmul0  19819  chfacfpmmul0  19823  cpmadugsumlemF  19837  tg2  19917  neindisj2  20076  neiptopnei  20085  t1t0  20301  fiuncmp  20356  hmeof1o  20716  ist1-5lem  20772  t1r0  20773  alexsublem  20996  imasdsf1olem  21325  tgioo  21751  fsumcn  21839  voliunlem3  22442  itgfsum  22721  dvbsss  22794  dvmptfsum  22864  dvfsumlem2  22916  dvfsumlem4  22918  plyco  23132  dgrcolem1  23164  dgrco  23166  dvntaylp  23263  taylthlem1  23265  jensen  23851  bposlem5  24153  lgsquad2lem2  24224  dchrisum0flb  24285  pntpbnd1  24361  pntlemf  24380  brbtwn  24866  brcgr  24867  ushgrauhgra  24967  uhgra0v  24974  umisuhgra  24991  usgrac  25015  uslgraf1oedg  25023  uslisushgra  25027  uslisumgra  25028  usisuslgra  25029  elusuhgra  25032  usgra0v  25035  usgranloopv  25042  usgranloop  25043  usgra1v  25054  usgraidx2vlem2  25056  usgrafisindb0  25073  usgrafisindb1  25074  usgrafisinds  25078  usgrafisbase  25079  iscusgra0  25122  cusgrasize2inds  25142  cusgrafi  25147  2mwlk  25186  iswlkg  25189  wlkcpr  25194  edgwlk  25196  trliswlk  25206  2trllemE  25220  usgrwlknloop  25230  pthistrl  25239  spthispth  25240  pthdepisspth  25241  redwlk  25273  wlkdvspth  25275  usgra2adedgspthlem2  25277  usgra2wlkspth  25286  crctistrl  25293  cyclispth  25294  cycliscrct  25295  cyclnspth  25296  cyclispthon  25298  fargshiftf  25301  fargshiftf1  25302  fargshiftfo  25303  usgrcyclnl1  25305  usgrcyclnl2  25306  nvnencycllem  25308  3v3e3cycl1  25309  constr3trllem5  25319  constr3trl  25324  constr3pth  25325  constr3cycl  25326  4cycl4v4e  25331  4cycl4dv4e  25333  cusconngra  25341  wwlknimp  25352  wwlkn0  25354  wlkiswwlk1  25355  wlkiswwlk2lem4  25359  wlkiswwlk2  25362  wlklniswwlkn2  25365  wwlkiswwlkn  25367  2wlkeq  25372  wwlknred  25388  wwlknext  25389  wwlknextbi  25390  wwlknredwwlkn0  25392  wwlkextwrd  25393  wwlkm1edg  25400  wwlkextproplem3  25408  isclwlkg  25420  clwlkswlks  25423  clwwlkprop  25435  clwwlkgt0  25436  clwwlknimp  25441  clwlkisclwwlklem2a  25450  clwlkisclwwlklem1  25452  clwwlkext2edg  25467  clwwisshclww  25472  clwwnisshclwwn  25474  usghashecclwwlk  25500  wlklenvclwlk  25504  2spontn0vne  25552  usg2spthonot  25553  usg2spthonot0  25554  usgfidegfi  25575  usgravd00  25584  rgraprop  25593  rusgraprop  25594  rusgrargra  25595  cusgraisrusgra  25603  0eusgraiff0rgracl  25606  rusgrasn  25610  rusgranumwlklem1  25614  eupatrl  25633  eupath2  25645  3vfriswmgra  25670  3cyclfrgrarn1  25677  3cyclfrgrarn  25678  n4cyclfrgra  25683  frgranbnb  25685  frconngra  25686  vdfrgra0  25687  vdn0frgrav2  25688  vdgn0frgrav2  25689  usgn0fidegnn0  25694  frgrancvvdeqlem4  25698  frgrancvvdeqlem7  25701  frgrancvvdeqlemA  25702  frgrancvvdeqlemB  25703  frgrawopreglem4  25712  frgrawopreglem5  25713  frgrawopreg  25714  frgraregorufr0  25717  frgraeu  25719  frg2wot1  25722  frg2woteqm  25724  frg2woteq  25725  frgregordn0  25735  numclwwlkun  25744  numclwwlk8  25780  frgrareggt1  25781  frgrareg  25782  frgraregord013  25783  frgraregord13  25784  frgraogt3nreg  25785  friendshipgt3  25786  friendship  25787  opidon2OLD  25989  isexid2  25990  grpomndo  26011  elghomlem2OLD  26027  rngoidmlem  26088  rngoueqz  26095  blocn2  26386  cvexchlem  27958  cdj3lem2b  28027  cnvoprab  28253  nnindf  28328  issgon  28892  sitgclg  29122  sseqp1  29175  bnj938  29695  bnj964  29701  bnj1052  29731  bnj1125  29748  subfacp1lem6  29855  cvmliftlem7  29961  cvmliftlem10  29964  mclsrcl  30146  pprodss4v  30595  segleantisym  30826  rankeq1o  30882  iooelexlt  31672  relowlssretop  31673  rdgeqoa  31680  poimirlem22  31869  poimirlem25  31872  poimirlem28  31875  poimirlem31  31878  mblfinlem3  31886  mbfresfi  31894  mettrifi  31993  iscringd  32139  cdlemk35s  34416  cdlemk39s  34418  cdlemk42  34420  mzpadd  35492  mzpmul  35493  mzpcompact2  35506  dford3lem2  35795  aomclem6  35830  cnsrexpcl  35944  relexpss1d  36210  iunrelexpmin1  36213  iunrelexpmin2  36217  nzin  36580  axc11next  36670  iotavalsb  36697  fperiodmullem  37418  fmul01  37541  fmulcl  37542  fmuldfeqlem1  37543  fmuldfeq  37544  iblspltprt  37733  itgspltprt  37739  stoweidlem2  37745  stoweidlem3  37746  stoweidlem6  37749  stoweidlem8  37751  stoweidlem17  37760  stoweidlem19  37762  stoweidlem21  37764  stoweidlem26  37769  stoweidlem31  37775  stoweidlem43  37787  fourierdlem42  37895  fourierdlem42OLD  37896  eu2ndop1stv  38437  funressnfv  38443  afv0fv0  38464  afv0nbfvbi  38466  smonoord  38531  mod2eq1n2dvds  38538  iccpartiltu  38549  iccpartigtl  38550  iccelpart  38560  icceuelpart  38563  bgoldbwt  38691  bgoldbtbndlem2  38714  bgoldbtbndlem4  38716  tgoldbach  38724  funopsn  38824  ssfz12  38851  fzoopth  38860  uspgrf1oedg  39018  usgrnloopv  39035  usgrnloop  39036  usgridx2vlem2  39050  subgrprop  39082  uvtxaisvtx  39192  vtxnbuvtx  39193  uvtxanbgrvtx  39195  cusgrsize2inds  39242  usgra2pthspth  39256  spthdifv  39257  usgra2pth  39259  uhgrasiz  39297  usgfis  39349  usgfisALT  39353  clcllaw  39418  intop  39430  clintop  39435  assintop  39436  assintopcllaw  39439  lmod0rng  39459  ringrng  39470  rngimf1o  39496  rngimrnghm  39497  ztprmneprm  39721  scmsuppss  39750  ply1mulgsumlem1  39771  ply1mulgsumlem2  39772  lcoel0  39814  ellcoellss  39821  lindslinindsimp2lem5  39848  ldepspr  39859  nno  39921  nn0o  39922  flnn0div2ge  39933  nnolog2flm1  39994  blengt1fldiv2p1  39997  dignn0flhalf  40022
  Copyright terms: Public domain W3C validator