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  2120  sbcn1  3351  sbcim1  3352  sbcbi1  3353  sbcel21v  3366  elimasni  5215  sotri  5247  relcoi1OLD  5385  unixpid  5391  f0rn0  5785  f1ocnv  5843  tz6.12c  5900  funbrfv  5919  f1dom3el3dif  6184  oprabid  6332  oprabv  6353  ndmovordi  6474  elovmpt2rab  6529  elovmpt2rab1  6530  elovmpt3rab1  6541  limomss  6711  unielxp  6843  f1o2ndf1  6915  smogt  7094  tfrlem1  7102  oawordeulem  7263  omass  7289  ecopovtrn  7474  php  7762  unxpdom  7785  findcard2d  7819  findcard3  7820  isfinite2  7835  fsuppimp  7895  fsuppunfi  7909  fsuppunbi  7910  fsuppres  7914  cantnfval2  8173  cantnfle  8175  cantnfp1lem3  8184  cantnflem1  8193  cnfcom  8204  rankr1ai  8268  rankonidlem  8298  rankxplim2  8350  oncard  8393  ficardom  8394  cardne  8398  acnnum  8481  alephord2i  8506  cardaleph  8518  aceq3lem  8549  dfac5lem5  8556  dfac12lem3  8573  cdainf  8620  ackbij1lem16  8663  cfslb  8694  cfslb2n  8696  cfsmolem  8698  fin4i  8726  infpssr  8736  fin1a2lem6  8833  axdc3lem2  8879  axcclem  8885  ttukeylem6  8942  fodomb  8952  gchi  9048  fpwwe2lem5  9058  pwfseqlem4  9086  pwfseq  9088  inawina  9114  wunfi  9145  inar1  9199  ltexnq  9399  ltbtwnnq  9402  ltexprlem4  9463  ltexpri  9467  prlem936  9471  suplem1pr  9476  suplem2pr  9477  recexsrlem  9526  mulgt0sr  9528  map2psrpr  9533  supsr  9535  eqlei  9743  eqlei2  9744  ledivp1i  10532  nnind  10627  nnmulcl  10632  nn0ge2m1nn  10934  nnnegz  10940  ublbneg  11248  xmulasslem  11571  ixxssixx  11649  iccshftri  11765  iccshftli  11767  iccdili  11769  icccntri  11771  1fv  11906  fzo1fzo0n0  11955  elfzonlteqm1  11986  ssfzo12  12001  zmodidfzoimp  12124  mptnn0fsuppr  12208  seqp1  12225  seqcl2  12228  seqfveq2  12232  seqshft2  12236  monoord  12240  seqsplit  12243  seqcaopr3  12245  seqf1olem2a  12248  seqf1o  12251  seqid2  12256  seqhomo  12257  hashf1rn  12532  hashinfxadd  12561  hashle00  12574  hashf1lem2  12614  seqcoll  12621  hash2pr  12624  pr2pwpr  12629  hash3tr  12638  brfi1uzind  12641  snopiswrd  12668  elovmptnn0wrd  12697  swrdswrd  12801  swrdccatin12lem2a  12826  swrdccat  12834  swrdccatin1d  12840  swrdccatin2d  12841  swrdccatin12d  12842  repswccat  12873  cshwidxmod  12890  relexpsucnnr  13067  rtrclreclem3  13102  rtrclreclem4  13103  dfrtrcl2  13104  relexpindlem  13105  relexpind  13106  rtrclind  13107  cjre  13181  climeu  13597  climub  13703  fsum2d  13810  fsumabs  13839  fsumrlim  13849  fsumo1  13850  fsumiun  13859  prodfn0  13928  prodfrec  13929  ntrivcvg  13931  fprodabs  14006  fprod2d  14013  fprodefsum  14127  ruclem9  14268  sadcadd  14406  sadadd2  14408  saddisjlem  14412  smuval2  14430  smupval  14436  smueqlem  14438  smumullem  14440  lcmgcdlem  14536  lcmftp  14571  exprmfct  14610  eulerthlem2  14690  pcmpt  14791  vdwlem10  14894  cshwsidrepsw  15018  cshwshashlem1  15020  prmlem1a  15032  ressval3d  15139  mreexexd  15496  letsr  16415  pmtrfrn  17041  pmtr3ncom  17058  gsmtrcl  17099  psgnsn  17103  sylow1lem1  17176  efginvrel2  17303  efgsrel  17310  cntzcmnss  17407  gsumzoppg  17503  gsum2dlem2  17529  telgsumfzs  17545  dprdval  17561  ablfac1eulem  17631  pgpfac1  17639  pgpfac  17643  srgpcomp  17691  ring1ne0  17747  rimf1o  17888  rimrhm  17889  brric2  17899  0ringnnzr  18419  mplcoe1  18615  mplcoe3  18616  mplcoe5lem  18617  mplcoe5  18618  mpfaddcl  18683  mpfmulcl  18684  coe1ae0  18735  coe1fzgsumd  18822  gsummoncoe1  18824  pf1addcl  18867  pf1mulcl  18868  evl1gsumd  18871  zrhpsgnelbas  19084  psgndiflemA  19091  mamufacex  19336  mat0dimcrng  19417  mavmulsolcl  19498  mdetunilem9  19567  cramerlem3  19636  pmatcollpw3fi1  19734  pm2mpfo  19760  chmaidscmat  19794  chfacfscmul0  19804  chfacfpmmul0  19808  cpmadugsumlemF  19822  tg2  19902  neindisj2  20061  neiptopnei  20070  t1t0  20286  fiuncmp  20341  hmeof1o  20701  ist1-5lem  20757  t1r0  20758  alexsublem  20981  imasdsf1olem  21310  tgioo  21716  fsumcn  21789  voliunlem3  22373  itgfsum  22652  dvbsss  22725  dvmptfsum  22795  dvfsumlem2  22847  dvfsumlem4  22849  plyco  23054  dgrcolem1  23086  dgrco  23088  dvntaylp  23182  taylthlem1  23184  jensen  23770  bposlem5  24070  lgsquad2lem2  24141  dchrisum0flb  24202  pntpbnd1  24278  pntlemf  24297  brbtwn  24766  brcgr  24767  ushgrauhgra  24867  uhgra0v  24874  umisuhgra  24891  usgrac  24915  uslgraf1oedg  24923  uslisushgra  24927  uslisumgra  24928  usisuslgra  24929  elusuhgra  24932  usgra0v  24935  usgranloopv  24942  usgranloop  24943  usgra1v  24954  usgraidx2vlem2  24956  usgrafisindb0  24972  usgrafisindb1  24973  usgrafisinds  24977  usgrafisbase  24978  iscusgra0  25021  cusgrasize2inds  25041  cusgrafi  25046  2mwlk  25085  iswlkg  25088  wlkcpr  25093  edgwlk  25095  trliswlk  25105  2trllemE  25119  usgrnloop  25129  pthistrl  25138  spthispth  25139  pthdepisspth  25140  redwlk  25172  wlkdvspth  25174  usgra2adedgspthlem2  25176  usgra2wlkspth  25185  crctistrl  25192  cyclispth  25193  cycliscrct  25194  cyclnspth  25195  cyclispthon  25197  fargshiftf  25200  fargshiftf1  25201  fargshiftfo  25202  usgrcyclnl1  25204  usgrcyclnl2  25205  nvnencycllem  25207  3v3e3cycl1  25208  constr3trllem5  25218  constr3trl  25223  constr3pth  25224  constr3cycl  25225  4cycl4v4e  25230  4cycl4dv4e  25232  cusconngra  25240  wwlknimp  25251  wwlkn0  25253  wlkiswwlk1  25254  wlkiswwlk2lem4  25258  wlkiswwlk2  25261  wlklniswwlkn2  25264  wwlkiswwlkn  25266  2wlkeq  25271  wwlknred  25287  wwlknext  25288  wwlknextbi  25289  wwlknredwwlkn0  25291  wwlkextwrd  25292  wwlkm1edg  25299  wwlkextproplem3  25307  isclwlkg  25319  clwlkswlks  25322  clwwlkprop  25334  clwwlkgt0  25335  clwwlknimp  25340  clwlkisclwwlklem2a  25349  clwlkisclwwlklem1  25351  clwwlkext2edg  25366  clwwisshclww  25371  clwwnisshclwwn  25373  usghashecclwwlk  25399  wlklenvclwlk  25403  2spontn0vne  25451  usg2spthonot  25452  usg2spthonot0  25453  usgfidegfi  25474  usgravd00  25483  rgraprop  25492  rusgraprop  25493  rusgrargra  25494  cusgraisrusgra  25502  0eusgraiff0rgracl  25505  rusgrasn  25509  rusgranumwlklem1  25513  eupatrl  25532  eupath2  25544  3vfriswmgra  25569  3cyclfrgrarn1  25576  3cyclfrgrarn  25577  n4cyclfrgra  25582  frgranbnb  25584  frconngra  25585  vdfrgra0  25586  vdn0frgrav2  25587  vdgn0frgrav2  25588  usgn0fidegnn0  25593  frgrancvvdeqlem4  25597  frgrancvvdeqlem7  25600  frgrancvvdeqlemA  25601  frgrancvvdeqlemB  25602  frgrawopreglem4  25611  frgrawopreglem5  25612  frgrawopreg  25613  frgraregorufr0  25616  frgraeu  25618  frg2wot1  25621  frg2woteqm  25623  frg2woteq  25624  frgregordn0  25634  numclwwlkun  25643  numclwwlk8  25679  frgrareggt1  25680  frgrareg  25681  frgraregord013  25682  frgraregord13  25683  frgraogt3nreg  25684  friendshipgt3  25685  friendship  25686  opidon2OLD  25888  isexid2  25889  grpomndo  25910  elghomlem2OLD  25926  rngoidmlem  25987  rngoueqz  25994  blocn2  26285  cvexchlem  27847  cdj3lem2b  27916  cnvoprab  28142  nnindf  28211  issgon  28775  sitgclg  28994  sseqp1  29045  bnj938  29527  bnj964  29533  bnj1052  29563  bnj1125  29580  subfacp1lem6  29687  cvmliftlem7  29793  cvmliftlem10  29796  mclsrcl  29978  pprodss4v  30427  segleantisym  30658  rankeq1o  30714  iooelexlt  31490  relowlssretop  31491  poimirlem22  31656  poimirlem25  31659  poimirlem28  31662  poimirlem31  31665  mblfinlem3  31673  mbfresfi  31681  mettrifi  31780  iscringd  31926  cdlemk35s  34203  cdlemk39s  34205  cdlemk42  34207  mzpadd  35279  mzpmul  35280  mzpcompact2  35293  dford3lem2  35578  aomclem6  35613  cnsrexpcl  35720  relexpss1d  35926  iunrelexpmin1  35929  iunrelexpmin2  35933  nzin  36294  axc11next  36384  iotavalsb  36411  fperiodmullem  37120  fmul01  37220  fmulcl  37221  fmuldfeqlem1  37222  fmuldfeq  37223  iblspltprt  37409  itgspltprt  37415  stoweidlem2  37421  stoweidlem3  37422  stoweidlem6  37425  stoweidlem8  37427  stoweidlem17  37436  stoweidlem19  37438  stoweidlem21  37440  stoweidlem26  37445  stoweidlem31  37451  stoweidlem43  37463  fourierdlem42  37570  eu2ndop1stv  38004  funressnfv  38010  afv0fv0  38031  afv0nbfvbi  38033  smonoord  38098  mod2eq1n2dvds  38105  iccpartiltu  38116  iccpartigtl  38117  iccelpart  38127  icceuelpart  38130  bgoldbwt  38258  bgoldbtbndlem2  38281  bgoldbtbndlem4  38283  tgoldbach  38291  ssfz12  38393  fzoopth  38402  usgra2pthspth  38411  spthdifv  38412  usgra2pth  38414  uhgrasiz  38454  usgfis  38506  usgfisALT  38510  clcllaw  38575  intop  38587  clintop  38592  assintop  38593  assintopcllaw  38596  lmod0rng  38616  ringrng  38627  rngimf1o  38653  rngimrnghm  38654  ztprmneprm  38878  scmsuppss  38907  ply1mulgsumlem1  38928  ply1mulgsumlem2  38929  lcoel0  38971  ellcoellss  38978  lindslinindsimp2lem5  39005  ldepspr  39016  nno  39079  nn0o  39080  flnn0div2ge  39091  nnolog2flm1  39152  blengt1fldiv2p1  39155  dignn0flhalf  39180
  Copyright terms: Public domain W3C validator