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  2050  sbcn1  3361  sbcim1  3362  sbcbi1  3363  sbcel21v  3381  elimasni  5354  sotri  5384  sotriOLD  5389  relcoi1  5526  unixpid  5532  f0rn0  5760  f1ocnv  5818  tz6.12c  5875  funbrfv  5896  f1dom3el3dif  6161  oprabid  6308  oprabv  6330  ndmovordi  6451  elovmpt2rab  6506  elovmpt2rab1  6507  elovmpt3rab1  6521  limomss  6690  unielxp  6821  f1o2ndf1  6893  smogt  7040  tfrlem1  7047  oawordeulem  7205  omass  7231  ecopovtrn  7416  php  7703  unxpdom  7729  findcard2d  7764  findcard3  7765  isfinite2  7780  fsuppimp  7837  fsuppunfi  7851  fsuppunbi  7852  fsuppres  7856  cantnfval2  8091  cantnfle  8093  cantnfp1lem3  8102  cantnflem1  8111  cantnfval2OLD  8121  cantnfleOLD  8123  cantnfp1lem3OLD  8128  cantnflem1OLD  8134  cnfcom  8147  cnfcomOLD  8155  rankr1ai  8219  rankonidlem  8249  rankxplim2  8301  oncard  8344  ficardom  8345  cardne  8349  acnnum  8436  alephord2i  8461  cardaleph  8473  aceq3lem  8504  dfac5lem5  8511  dfac12lem3  8528  cdainf  8575  ackbij1lem16  8618  cfslb  8649  cfslb2n  8651  cfsmolem  8653  fin4i  8681  infpssr  8691  fin1a2lem6  8788  axdc3lem2  8834  axcclem  8840  ttukeylem6  8897  fodomb  8907  gchi  9005  fpwwe2lem5  9015  pwfseqlem4  9043  pwfseq  9045  inawina  9071  wunfi  9102  inar1  9156  ltexnq  9356  ltbtwnnq  9359  ltexprlem4  9420  ltexpri  9424  prlem936  9428  suplem1pr  9433  suplem2pr  9434  recexsrlem  9483  mulgt0sr  9485  map2psrpr  9490  supsr  9492  eqlei  9697  eqlei2  9698  ledivp1i  10477  nnind  10560  nnmulcl  10565  nn0ge2m1nn  10867  nnnegz  10873  uzindOLD  10963  ublbneg  11175  xmulasslem  11486  ixxssixx  11552  iccshftri  11664  iccshftli  11666  iccdili  11668  icccntri  11670  1fv  11800  fzo1fzo0n0  11843  elfzonlteqm1  11870  ssfzo12  11884  zmodidfzoimp  12005  mptnn0fsuppr  12084  seqp1  12101  seqcl2  12104  seqfveq2  12108  seqshft2  12112  monoord  12116  seqsplit  12119  seqcaopr3  12121  seqf1olem2a  12124  seqf1o  12127  seqid2  12132  seqhomo  12133  hashf1rn  12404  hashinfxadd  12432  hashle00  12444  hashf1lem2  12484  seqcoll  12491  hash2pr  12494  pr2pwpr  12499  hash3tr  12508  brfi1uzind  12511  snopiswrd  12535  elovmptnn0wrd  12563  swrdswrd  12664  swrdccatin12lem2a  12689  swrdccat  12697  swrdccatin1d  12703  swrdccatin2d  12704  swrdccatin12d  12705  repswccat  12736  cshwidxmod  12753  cjre  12951  climeu  13357  climub  13463  fsum2d  13565  fsumabs  13594  fsumrlim  13604  fsumo1  13605  fsumiun  13614  ruclem9  13848  sadcadd  13985  sadadd2  13987  saddisjlem  13991  smuval2  14009  smupval  14015  smueqlem  14017  smumullem  14019  exprmfct  14128  eulerthlem2  14189  pcmpt  14288  vdwlem10  14385  cshwsidrepsw  14455  cshwshashlem1  14457  prmlem1a  14469  mreexexd  14922  letsr  15731  pmtrfrn  16357  pmtr3ncom  16374  gsmtrcl  16415  psgnsn  16419  sylow1lem1  16492  efginvrel2  16619  efgsrel  16626  cntzcmnss  16723  gsumzoppg  16841  gsum2dlem2  16872  gsum2dOLD  16874  telgsumfzs  16892  dprdval  16908  dprdvalOLD  16910  ablfac1eulem  16997  pgpfac1  17005  pgpfac  17009  srgpcomp  17057  ring1ne0  17113  rimf1o  17257  rimrhm  17258  brric2  17268  0ringnnzr  17791  mplcoe1  18001  mplcoe3  18002  mplcoe3OLD  18003  mplcoe5lem  18004  mplcoe5  18005  mplcoe2OLD  18007  mpfaddcl  18077  mpfmulcl  18078  coe1ae0  18131  coe1fzgsumd  18218  gsummoncoe1  18220  pf1addcl  18263  pf1mulcl  18264  evl1gsumd  18267  zrhpsgnelbas  18503  psgndiflemA  18510  mamufacex  18764  mat0dimcrng  18845  mavmulsolcl  18926  mdetunilem9  18995  cramerlem3  19064  pmatcollpw3fi1  19162  pm2mpfo  19188  chmaidscmat  19222  chfacfscmul0  19232  chfacfpmmul0  19236  cpmadugsumlemF  19250  tg2  19339  neindisj2  19497  neiptopnei  19506  t1t0  19722  fiuncmp  19777  bwthOLD  19784  hmeof1o  20138  ist1-5lem  20194  t1r0  20195  alexsublem  20417  imasdsf1olem  20749  tgioo  21174  fsumcn  21247  voliunlem3  21835  itgfsum  22106  dvbsss  22179  dvmptfsum  22249  dvfsumlem2  22301  dvfsumlem4  22303  plyco  22511  dgrcolem1  22542  dgrco  22544  dvntaylp  22638  taylthlem1  22640  jensen  23190  bposlem5  23435  lgsquad2lem2  23506  dchrisum0flb  23567  pntpbnd1  23643  pntlemf  23662  brbtwn  24074  brcgr  24075  ushgrauhgra  24175  uhgra0v  24182  umisuhgra  24199  usgrac  24223  uslgraf1oedg  24231  uslisushgra  24235  uslisumgra  24236  usisuslgra  24237  elusuhgra  24240  usgra0v  24243  usgranloopv  24250  usgranloop  24251  usgra1v  24262  usgraidx2vlem2  24264  usgrafisindb0  24280  usgrafisindb1  24281  usgrafisinds  24285  usgrafisbase  24286  iscusgra0  24329  cusgrasize2inds  24349  cusgrafi  24354  2mwlk  24393  iswlkg  24396  wlkcpr  24401  edgwlk  24403  trliswlk  24413  2trllemE  24427  usgrnloop  24437  pthistrl  24446  spthispth  24447  pthdepisspth  24448  redwlk  24480  wlkdvspth  24482  usgra2adedgspthlem2  24484  usgra2wlkspth  24493  crctistrl  24500  cyclispth  24501  cycliscrct  24502  cyclnspth  24503  cyclispthon  24505  fargshiftf  24508  fargshiftf1  24509  fargshiftfo  24510  usgrcyclnl1  24512  usgrcyclnl2  24513  nvnencycllem  24515  3v3e3cycl1  24516  constr3trllem5  24526  constr3trl  24531  constr3pth  24532  constr3cycl  24533  4cycl4v4e  24538  4cycl4dv4e  24540  cusconngra  24548  wwlknimp  24559  wwlkn0  24561  wlkiswwlk1  24562  wlkiswwlk2lem4  24566  wlkiswwlk2  24569  wlklniswwlkn2  24572  wwlkiswwlkn  24574  2wlkeq  24579  wwlknred  24595  wwlknext  24596  wwlknextbi  24597  wwlknredwwlkn0  24599  wwlkextwrd  24600  wwlkm1edg  24607  wwlkextproplem3  24615  isclwlkg  24627  clwlkswlks  24630  clwwlkprop  24642  clwwlkgt0  24643  clwwlknimp  24648  clwlkisclwwlklem2a  24657  clwlkisclwwlklem1  24659  clwwlkext2edg  24674  clwwisshclww  24679  clwwnisshclwwn  24681  usghashecclwwlk  24707  wlklenvclwlk  24711  2spontn0vne  24759  usg2spthonot  24760  usg2spthonot0  24761  usgfidegfi  24782  usgravd00  24791  rgraprop  24800  rusgraprop  24801  rusgrargra  24802  cusgraisrusgra  24810  0eusgraiff0rgracl  24813  rusgrasn  24817  rusgranumwlklem1  24821  eupatrl  24840  eupath2  24852  3vfriswmgra  24877  3cyclfrgrarn1  24884  3cyclfrgrarn  24885  n4cyclfrgra  24890  frgranbnb  24892  frconngra  24893  vdfrgra0  24894  vdn0frgrav2  24895  vdgn0frgrav2  24896  usgn0fidegnn0  24901  frgrancvvdeqlem4  24905  frgrancvvdeqlem7  24908  frgrancvvdeqlemA  24909  frgrancvvdeqlemB  24910  frgrawopreglem4  24919  frgrawopreglem5  24920  frgrawopreg  24921  frgraregorufr0  24924  frgraeu  24926  frg2wot1  24929  frg2woteqm  24931  frg2woteq  24932  frgregordn0  24942  numclwwlkun  24951  numclwwlk8  24987  frgrareggt1  24988  frgrareg  24989  frgraregord013  24990  frgraregord13  24991  frgraogt3nreg  24992  friendshipgt3  24993  friendship  24994  opidon2OLD  25198  isexid2  25199  grpomndo  25220  elghomlem2OLD  25236  rngoidmlem  25297  rngoueqz  25304  blocn2  25595  cvexchlem  27159  cdj3lem2b  27228  cnvoprab  27418  nnindf  27483  issgon  27996  sitgclg  28157  sseqp1  28207  subfacp1lem6  28502  cvmliftlem7  28609  cvmliftlem10  28612  mclsrcl  28794  relexp0  28925  relexpsucr  28926  relexpsucl  28928  relexprel  28930  relexpdm  28931  relexprn  28932  relexpadd  28934  relexpindlem  28935  relexpind  28936  rtrclreclem.trans  28942  rtrclreclem.min  28943  dfrtrcl2  28944  rtrclind  28945  prodfn0  29003  prodfrec  29004  ntrivcvg  29006  fprodabs  29078  fprodefsum  29079  fprod2d  29086  pprodss4v  29509  segleantisym  29740  rankeq1o  29803  mblfinlem3  30028  mbfresfi  30036  mettrifi  30225  iscringd  30371  mzpadd  30645  mzpmul  30646  mzpcompact2  30660  dford3lem2  30944  aomclem6  30980  cnsrexpcl  31090  lcmgcdlem  31188  nzin  31199  axc11next  31267  iotavalsb  31294  fperiodmullem  31452  fmul01  31502  fmulcl  31503  fmuldfeqlem1  31504  fmuldfeq  31505  iblspltprt  31662  itgspltprt  31668  stoweidlem2  31673  stoweidlem3  31674  stoweidlem6  31677  stoweidlem8  31679  stoweidlem17  31688  stoweidlem19  31690  stoweidlem21  31692  stoweidlem26  31697  stoweidlem31  31702  stoweidlem43  31714  fourierdlem42  31820  eu2ndop1stv  32045  funressnfv  32051  afv0fv0  32072  afv0nbfvbi  32074  ssfz12  32168  fzoopth  32178  usgra2pthspth  32189  spthdifv  32190  usgra2pth  32192  uhgrasiz  32232  usgfis  32284  usgfisALT  32288  clcllaw  32352  intop  32364  clintop  32369  assintop  32370  assintopcllaw  32373  ressval3d  32393  ringrng  32406  rngimf1o  32429  rngimrnghm  32430  ztprmneprm  32669  lmod0rng  32694  scmsuppss  32700  ply1mulgsumlem1  32721  ply1mulgsumlem2  32722  lcoel0  32764  ellcoellss  32771  lindslinindsimp2lem5  32798  ldepspr  32809  bnj938  33728  bnj964  33734  bnj1052  33764  bnj1125  33781  cdlemk35s  36403  cdlemk39s  36405  cdlemk42  36407
  Copyright terms: Public domain W3C validator