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

Theorem mpcom 36
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 31 . 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  470  axc16i  2030  sbcn1  3372  sbcim1  3373  sbcbi1  3374  sbcel21v  3392  elimasni  5355  sotri  5385  sotriOLD  5390  relcoi1  5527  unixpid  5533  f0rn0  5761  f1ocnv  5819  tz6.12c  5876  funbrfv  5897  f1dom3el3dif  6155  oprabid  6299  oprabv  6320  ndmovordi  6441  elovmpt2rab  6496  elovmpt2rab1  6497  elovmpt3rab1  6511  limomss  6676  unielxp  6810  f1o2ndf1  6881  smogt  7028  tfrlem1  7035  oawordeulem  7193  omass  7219  ecopovtrn  7404  php  7691  unxpdom  7717  findcard2d  7751  findcard3  7752  isfinite2  7767  fsuppimp  7824  fsuppunfi  7838  fsuppunbi  7839  fsuppres  7843  cantnfval2  8077  cantnfle  8079  cantnfp1lem3  8088  cantnflem1  8097  cantnfval2OLD  8107  cantnfleOLD  8109  cantnfp1lem3OLD  8114  cantnflem1OLD  8120  cnfcom  8133  cnfcomOLD  8141  rankr1ai  8205  rankonidlem  8235  rankxplim2  8287  oncard  8330  ficardom  8331  cardne  8335  acnnum  8422  alephord2i  8447  cardaleph  8459  aceq3lem  8490  dfac5lem5  8497  dfac12lem3  8514  cdainf  8561  ackbij1lem16  8604  cfslb  8635  cfslb2n  8637  cfsmolem  8639  fin4i  8667  infpssr  8677  fin1a2lem6  8774  axdc3lem2  8820  axcclem  8826  ttukeylem6  8883  fodomb  8893  gchi  8991  fpwwe2lem5  9001  pwfseqlem4  9029  pwfseq  9031  inawina  9057  wunfi  9088  inar1  9142  ltexnq  9342  ltbtwnnq  9345  ltexprlem4  9406  ltexpri  9410  prlem936  9414  suplem1pr  9419  suplem2pr  9420  recexsrlem  9469  mulgt0sr  9471  map2psrpr  9476  supsr  9478  eqlei  9683  eqlei2  9684  ledivp1i  10460  nnind  10543  nnmulcl  10548  nn0ge2m1nn  10850  nnnegz  10856  uzindOLD  10944  ublbneg  11155  xmulasslem  11466  ixxssixx  11532  iccshftri  11644  iccshftli  11646  iccdili  11648  icccntri  11650  1fv  11778  fzo1fzo0n0  11821  elfzonlteqm1  11848  ssfzo12  11862  zmodidfzoimp  11982  mptnn0fsuppr  12061  seqp1  12078  seqcl2  12081  seqfveq2  12085  seqshft2  12089  monoord  12093  seqsplit  12096  seqcaopr3  12098  seqf1olem2a  12101  seqf1o  12104  seqid2  12109  seqhomo  12110  hashf1rn  12380  hashinfxadd  12408  hashle00  12418  hashf1lem2  12458  seqcoll  12465  hash2pr  12468  pr2pwpr  12473  hash3tr  12482  brfi1uzind  12485  snopiswrd  12509  elovmptnn0wrd  12536  swrdswrd  12635  swrdccatin12lem2a  12660  swrdccat  12668  swrdccatin1d  12674  swrdccatin2d  12675  swrdccatin12d  12676  repswccat  12707  cshwidxmod  12724  cjre  12922  climeu  13327  climub  13433  fsum2d  13535  fsumabs  13564  fsumrlim  13574  fsumo1  13575  fsumiun  13584  ruclem9  13821  sadcadd  13956  sadadd2  13958  saddisjlem  13962  smuval2  13980  smupval  13986  smueqlem  13988  smumullem  13990  exprmfct  14099  eulerthlem2  14160  pcmpt  14259  vdwlem10  14356  cshwsidrepsw  14425  cshwshashlem1  14427  prmlem1a  14439  mreexexd  14892  letsr  15703  pmtrfrn  16272  pmtr3ncom  16289  gsmtrcl  16330  psgnsn  16334  sylow1lem1  16407  efginvrel2  16534  efgsrel  16541  cntzcmnss  16635  gsumzmhm  16741  gsumzoppg  16751  gsum2dlem2  16782  gsum2dOLD  16784  telgsumfzs  16802  dprdval  16818  dprdvalOLD  16820  ablfac1eulem  16906  pgpfac1  16914  pgpfac  16918  srgpcomp  16964  rimf1o  17159  rimrhm  17160  brric2  17170  mplcoe1  17891  mplcoe3  17892  mplcoe3OLD  17893  mplcoe5lem  17894  mplcoe5  17895  mplcoe2OLD  17897  mpfaddcl  17967  mpfmulcl  17968  coe1ae0  18021  coe1fzgsumd  18108  gsummoncoe1  18110  pf1addcl  18153  pf1mulcl  18154  evl1gsumd  18157  zrhpsgnelbas  18390  psgndiflemA  18397  mamufacex  18651  mat0dimcrng  18732  mavmulsolcl  18813  mdetunilem9  18882  cramerlem3  18951  pmatcollpw3fi1  19049  pm2mpfo  19075  chmaidscmat  19109  fvmptnn04if  19110  chfacfscmul0  19119  chfacfpmmul0  19123  cpmadugsumlemF  19137  tg2  19226  neindisj2  19383  neiptopnei  19392  t1t0  19608  fiuncmp  19663  bwthOLD  19670  hmeof1o  19993  ist1-5lem  20049  t1r0  20050  alexsublem  20272  imasdsf1olem  20604  tgioo  21029  fsumcn  21102  voliunlem3  21690  itgfsum  21961  dvbsss  22034  dvmptfsum  22104  dvfsumlem2  22156  dvfsumlem4  22158  plyco  22366  dgrcolem1  22397  dgrco  22399  dvntaylp  22493  taylthlem1  22495  jensen  23039  bposlem5  23284  lgsquad2lem2  23355  dchrisum0flb  23416  pntpbnd1  23492  pntlemf  23511  brbtwn  23871  brcgr  23872  uhgra0v  23973  umisuhgra  23990  usgracl  24014  uslgraf1oedg  24022  uslisumgra  24026  usisuslgra  24027  elusuhgra  24030  usgra0v  24033  usgranloopv  24040  usgranloop  24041  usgra1v  24052  usgraidx2vlem2  24054  usgrafisindb0  24070  usgrafisindb1  24071  usgrafisinds  24075  usgrafisbase  24076  iscusgra0  24119  cusgrasize2inds  24139  cusgrafi  24144  2mwlk  24183  iswlkg  24186  wlkcpr  24191  edgwlk  24193  trliswlk  24203  2trllemE  24217  usgrnloop  24227  pthistrl  24236  spthispth  24237  pthdepisspth  24238  redwlk  24270  wlkdvspth  24272  usgra2adedgspthlem2  24274  usgra2wlkspth  24283  crctistrl  24290  cyclispth  24291  cycliscrct  24292  cyclnspth  24293  cyclispthon  24295  fargshiftf  24298  fargshiftf1  24299  fargshiftfo  24300  usgrcyclnl1  24302  usgrcyclnl2  24303  nvnencycllem  24305  3v3e3cycl1  24306  constr3trllem5  24316  constr3trl  24321  constr3pth  24322  constr3cycl  24323  4cycl4v4e  24328  4cycl4dv4e  24330  cusconngra  24338  wwlknimp  24349  wwlkn0  24351  wlkiswwlk1  24352  wlkiswwlk2lem4  24356  wlkiswwlk2  24359  wlklniswwlkn2  24362  wwlkiswwlkn  24364  2wlkeq  24369  wwlknred  24385  wwlknext  24386  wwlknextbi  24387  wwlknredwwlkn0  24389  wwlkextwrd  24390  wwlkm1edg  24397  wwlkextproplem3  24405  isclwlkg  24417  clwlkswlks  24420  clwwlkprop  24432  clwwlkgt0  24433  clwwlknimp  24438  clwlkisclwwlklem2a  24447  clwlkisclwwlklem1  24449  clwwlkext2edg  24464  clwwisshclww  24469  clwwnisshclwwn  24471  usghashecclwwlk  24497  wlklenvclwlk  24501  2spontn0vne  24549  usg2spthonot  24550  usg2spthonot0  24551  usgfidegfi  24572  usgravd00  24581  rgraprop  24590  rusgraprop  24591  rusgrargra  24592  cusgraisrusgra  24600  0eusgraiff0rgracl  24603  rusgrasn  24607  rusgranumwlklem1  24611  eupatrl  24630  eupath2  24642  opidon2  24852  isexid2  24853  grpomndo  24874  elghomlem2  24890  rngoidmlem  24951  rngoueqz  24958  blocn2  25249  cvexchlem  26813  cdj3lem2b  26882  cnvoprab  27068  nnindf  27128  issgon  27613  sitgclg  27774  sseqp1  27824  subfacp1lem6  28119  cvmliftlem7  28226  cvmliftlem10  28229  relexp0  28377  relexpsucr  28378  relexpsucl  28380  relexprel  28382  relexpdm  28383  relexprn  28384  relexpadd  28386  relexpindlem  28387  relexpind  28388  rtrclreclem.trans  28394  rtrclreclem.min  28395  dfrtrcl2  28396  rtrclind  28397  prodfn0  28455  prodfrec  28456  ntrivcvg  28458  fprodabs  28530  fprodefsum  28531  fprod2d  28538  pprodss4v  28961  segleantisym  29192  rankeq1o  29255  mblfinlem3  29481  mbfresfi  29489  mettrifi  29704  iscringd  29850  mzpadd  30125  mzpmul  30126  mzpcompact2  30140  dford3lem2  30426  aomclem6  30462  cnsrexpcl  30572  axc11next  30710  iotavalsb  30737  fperiodmullem  30899  fmul01  30949  fmulcl  30950  fmuldfeqlem1  30951  fmuldfeq  30952  iblspltprt  31110  itgspltprt  31116  stoweidlem2  31121  stoweidlem3  31122  stoweidlem6  31125  stoweidlem8  31127  stoweidlem17  31136  stoweidlem19  31138  stoweidlem21  31140  stoweidlem26  31145  stoweidlem31  31150  stoweidlem43  31162  fourierdlem42  31268  fourierdlem89  31315  fourierdlem90  31316  fourierdlem91  31317  eu2ndop1stv  31493  funressnfv  31499  afv0fv0  31520  afv0nbfvbi  31522  ssfz12  31618  fzoopth  31628  usgra2pthspth  31639  spthdifv  31640  usgra2pth  31642  uhgrasiz  31661  usgfis  31704  3vfriswmgra  31723  3cyclfrgrarn1  31730  3cyclfrgrarn  31731  n4cyclfrgra  31736  frgranbnb  31738  frconngra  31739  vdfrgra0  31740  vdgfrgra0  31741  vdn0frgrav2  31742  vdgn0frgrav2  31743  usgn0fidegnn0  31748  frgrancvvdeqlem4  31752  frgrancvvdeqlem7  31755  frgrancvvdeqlemA  31756  frgrancvvdeqlemB  31757  frgrawopreglem2  31764  frgrawopreglem4  31766  frgrawopreglem5  31767  frgrawopreg  31768  frgraregorufr0  31771  frgraeu  31773  frg2wot1  31776  frg2woteqm  31778  frg2woteq  31779  frgregordn0  31789  numclwwlkun  31798  numclwwlk8  31834  frgrareggt1  31835  frgrareg  31836  frgraregord013  31837  frgraregord13  31838  frgraogt3nreg  31839  friendshipgt3  31840  friendship  31841  mndmgm  31850  ringrng0  31857  ztprmneprm  31875  rng1ne0  31901  0rngnnzr  31906  lmod0rng  31907  scmsuppss  31913  ply1mulgsumlem1  31934  ply1mulgsumlem2  31935  lcoel0  31977  ellcoellss  31984  lindslinindsimp2lem5  32011  ldepspr  32022  bnj938  32949  bnj964  32955  bnj1052  32985  bnj1125  33002  cdlemk35s  35608  cdlemk39s  35610  cdlemk42  35612
  Copyright terms: Public domain W3C validator