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  467  axc16i  2011  sbcn1  3222  sbcim1  3223  sbcbi1  3224  sbcel21v  3242  elimasni  5184  sotri  5213  sotriOLD  5218  relcoi1  5354  unixpid  5360  f1ocnv  5641  tz6.12c  5697  funbrfv  5718  f1dom3el3dif  5968  oprabid  6104  ndmovordi  6243  limomss  6470  unielxp  6601  f1o2ndf1  6669  smogt  6814  tfrlem1  6821  oawordeulem  6981  omass  7007  ecopovtrn  7191  php  7483  unxpdom  7508  findcard2d  7542  findcard3  7543  isfinite2  7558  fsuppimp  7614  fsuppunfi  7628  fsuppunbi  7629  fsuppres  7633  cantnfval2  7865  cantnfle  7867  cantnfp1lem3  7876  cantnflem1  7885  cantnfval2OLD  7895  cantnfleOLD  7897  cantnfp1lem3OLD  7902  cantnflem1OLD  7908  cnfcom  7921  cnfcomOLD  7929  rankr1ai  7993  rankonidlem  8023  rankxplim2  8075  oncard  8118  ficardom  8119  cardne  8123  acnnum  8210  alephord2i  8235  cardaleph  8247  aceq3lem  8278  dfac5lem5  8285  dfac12lem3  8302  cdainf  8349  ackbij1lem16  8392  cfslb  8423  cfslb2n  8425  cfsmolem  8427  fin4i  8455  infpssr  8465  fin1a2lem6  8562  axdc3lem2  8608  axcclem  8614  ttukeylem6  8671  fodomb  8681  gchi  8778  fpwwe2lem5  8788  pwfseqlem4  8816  pwfseq  8818  inawina  8844  wunfi  8875  inar1  8929  ltexnq  9131  ltbtwnnq  9134  ltexprlem4  9195  ltexpri  9199  prlem936  9203  suplem1pr  9208  suplem2pr  9209  recexsrlem  9257  mulgt0sr  9259  map2psrpr  9264  supsr  9266  eqlei  9471  eqlei2  9472  ledivp1i  10245  nnind  10327  nnmulcl  10332  nnnegz  10636  uzindOLD  10723  ublbneg  10926  xmulasslem  11235  ixxssixx  11301  iccshftri  11406  iccshftli  11408  iccdili  11410  icccntri  11412  1fv  11515  fzo1fzo0n0  11571  ssfzo12  11603  zmodidfzoimp  11721  seqp1  11804  seqcl2  11807  seqfveq2  11811  seqshft2  11815  monoord  11819  seqsplit  11822  seqcaopr3  11824  seqf1olem2a  11827  seqf1o  11830  seqid2  11835  seqhomo  11836  hashf1rn  12106  hashinfxadd  12131  hashle00  12141  hash2pr  12161  pr2pwpr  12166  hashf1lem2  12192  seqcoll  12199  brfi1uzind  12202  snopiswrd  12226  wrdlenfi  12241  swrdswrd  12337  swrdccatin12lem2a  12359  swrdccat  12367  swrdccatin1d  12373  swrdccatin2d  12374  swrdccatin12d  12375  repswccat  12406  cshwidxmod  12423  cjre  12611  climeu  13016  climub  13122  fsum2d  13221  fsumabs  13246  fsumrlim  13256  fsumo1  13257  fsumiun  13266  ruclem9  13502  sadcadd  13636  sadadd2  13638  saddisjlem  13642  smuval2  13660  smupval  13666  smueqlem  13668  smumullem  13670  exprmfct  13778  eulerthlem2  13839  pcmpt  13936  vdwlem10  14033  cshwsidrepsw  14102  cshwshashlem1  14104  prmlem1a  14116  mreexexd  14568  letsr  15379  pmtrfrn  15943  pmtr3ncom  15960  gsmtrcl  16001  sylow1lem1  16076  efginvrel2  16203  efgsrel  16210  cntzcmnss  16304  gsumzmhm  16406  gsumzoppg  16415  gsumunsnd  16426  gsum2dlem2  16435  gsum2dOLD  16437  dprdval  16458  dprdvalOLD  16460  ablfac1eulem  16546  pgpfac1  16554  pgpfac  16558  mplcoe1  17477  mplcoe3  17478  mplcoe3OLD  17479  mplcoe2  17480  mplcoe2OLD  17481  zrhpsgnelbas  17865  psgndiflemA  17872  mamufacex  18130  mavmulsolcl  18203  mdetunilem9  18267  cramerlem3  18336  tg2  18411  neindisj2  18568  neiptopnei  18577  t1t0  18793  fiuncmp  18848  bwthOLD  18855  hmeof1o  19178  ist1-5lem  19234  t1r0  19235  alexsublem  19457  imasdsf1olem  19789  tgioo  20214  fsumcn  20287  voliunlem3  20874  itgfsum  21145  dvbsss  21218  dvmptfsum  21288  dvfsumlem2  21340  dvfsumlem4  21342  mpfaddcl  21393  mpfmulcl  21394  pf1addcl  21403  pf1mulcl  21404  plyco  21593  dgrcolem1  21624  dgrco  21626  dvntaylp  21720  taylthlem1  21722  jensen  22266  bposlem5  22511  lgsquad2lem2  22582  dchrisum0flb  22643  pntpbnd1  22719  pntlemf  22738  brbtwn  22967  brcgr  22968  uhgra0v  23066  umisuhgra  23083  uslisumgra  23107  usisuslgra  23108  usgra0v  23112  usgranloopv  23119  usgranloop  23120  usgra1v  23130  usgraidx2vlem2  23132  usgrafisindb0  23143  usgrafisindb1  23144  usgrafisinds  23148  usgrafisbase  23149  iscusgra0  23187  cusgrasize2inds  23207  cusgrafi  23212  2mwlk  23249  trliswlk  23260  2trllemE  23274  usgrnloop  23284  pthistrl  23293  spthispth  23294  pthdepisspth  23295  redwlk  23327  wlkdvspth  23329  crctistrl  23336  cyclispth  23337  cycliscrct  23338  cyclnspth  23339  cyclispthon  23341  fargshiftf  23344  fargshiftf1  23345  fargshiftfo  23346  usgrcyclnl1  23348  usgrcyclnl2  23349  nvnencycllem  23351  3v3e3cycl1  23352  constr3trllem5  23362  constr3trl  23367  constr3pth  23368  constr3cycl  23369  4cycl4v4e  23374  4cycl4dv4e  23376  cusconngra  23384  eupatrl  23411  eupath2  23423  opidon2  23633  isexid2  23634  grpomndo  23655  elghomlem2  23671  rngoidmlem  23732  rngoueqz  23739  blocn2  24030  cvexchlem  25594  cdj3lem2b  25663  cnvoprab  25846  nnindf  25911  issgon  26419  sitgclg  26575  sseqp1  26625  subfacp1lem6  26920  cvmliftlem7  27027  cvmliftlem10  27030  relexp0  27177  relexpsucr  27178  relexpsucl  27180  relexprel  27182  relexpdm  27183  relexprn  27184  relexpadd  27186  relexpindlem  27187  relexpind  27188  rtrclreclem.trans  27194  rtrclreclem.min  27195  dfrtrcl2  27196  rtrclind  27197  prodfn0  27255  prodfrec  27256  ntrivcvg  27258  fprodabs  27330  fprodefsum  27331  fprod2d  27338  pprodss4v  27761  segleantisym  27992  rankeq1o  28055  mblfinlem3  28271  mbfresfi  28279  mettrifi  28494  iscringd  28640  mzpadd  28916  mzpmul  28917  mzpcompact2  28931  dford3lem2  29218  aomclem6  29254  cnsrexpcl  29364  axc11next  29502  iotavalsb  29529  fmul01  29603  fmulcl  29604  fmuldfeqlem1  29605  fmuldfeq  29606  stoweidlem2  29640  stoweidlem3  29641  stoweidlem6  29644  stoweidlem8  29646  stoweidlem17  29655  stoweidlem19  29657  stoweidlem21  29659  stoweidlem26  29664  stoweidlem31  29669  stoweidlem43  29681  eu2ndop1stv  29869  funressnfv  29877  afv0fv0  29898  afv0nbfvbi  29900  f0rn0  29984  oprabv  30000  elovmpt2rab  30001  elovmpt2rab1  30002  elovmpt3rab1  30006  ssfz12  30040  fzoopth  30056  elfzonlteqm1  30068  hash3tr  30077  elovmptnn0wrd  30100  iswlkg  30128  2wlkeq  30131  wlkcpr  30133  edgwlk  30137  usgra2pthspth  30138  usgra2wlkspth  30141  spthdifv  30142  usgra2pth  30144  usgra2adedgspthlem2  30147  wwlknimp  30164  wwlkn0  30166  wlkiswwlk1  30167  wlkiswwlk2lem4  30171  wlkiswwlk2  30174  wlklniswwlkn2  30177  wwlkiswwlkn  30179  wwlknred  30198  wwlknext  30199  wwlknextbi  30200  wwlknredwwlkn0  30202  wwlkextwrd  30203  wwlkm1edg  30210  2spontn0vne  30249  usg2spthonot  30250  usg2spthonot0  30251  isclwlkg  30263  clwlkswlks  30266  clwwlkprop  30276  clwwlkgt0  30277  clwwlknimp  30282  clwlkisclwwlklem2a  30290  clwlkisclwwlklem1  30292  clwwlkext2edg  30307  clwwisshclww  30314  clwwnisshclwwn  30316  usghashecclwwlk  30352  wlkp1lenfislenp  30355  usgfidegfi  30370  usgravd00  30381  rgraprop  30388  rusgraprop  30389  rusgrargra  30390  cusgraisrusgra  30394  rusgrasn  30400  wwlkextproplem3  30405  rusgranumwlklem1  30410  3vfriswmgra  30440  3cyclfrgrarn1  30447  3cyclfrgrarn  30448  n4cyclfrgra  30453  frgranbnb  30455  frconngra  30456  vdfrgra0  30457  vdgfrgra0  30458  vdn0frgrav2  30459  vdgn0frgrav2  30460  usgn0fidegnn0  30465  frgrancvvdeqlem4  30469  frgrancvvdeqlem7  30472  frgrancvvdeqlemA  30473  frgrancvvdeqlemB  30474  frgrawopreglem2  30481  frgrawopreglem4  30483  frgrawopreglem5  30484  frgrawopreg  30485  frgraregorufr0  30488  frgraeu  30490  frg2wot1  30493  frg2woteqm  30495  frg2woteq  30496  frgregordn0  30506  numclwwlkun  30515  numclwwlk8  30551  frgrareggt1  30552  frgrareg  30553  frgraregord013  30554  frgraregord13  30555  frgraogt3nreg  30556  friendshipgt3  30557  friendship  30558  ztprmneprm  30580  psgnsn  30599  rng1ne0  30601  0rngnnzr  30606  lmod0rng  30607  scmsuppss  30613  mat0dimcrng  30643  lcoel0  30668  ellcoellss  30675  lindslinindsimp2lem5  30702  ldepspr  30713  bnj938  31629  bnj964  31635  bnj1052  31665  bnj1125  31682  cdlemk35s  34151  cdlemk39s  34153  cdlemk42  34155
  Copyright terms: Public domain W3C validator