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  468  axc16i  2070  sbcn1  3298  sbcim1  3299  sbcbi1  3300  sbcel21v  3313  elimasni  5276  sotri  5307  relcoi1OLD  5445  unixpid  5451  f0rn0  5678  f1ocnv  5736  tz6.12c  5793  funbrfv  5812  f1dom3el3dif  6077  oprabid  6223  oprabv  6244  ndmovordi  6365  elovmpt2rab  6420  elovmpt2rab1  6421  elovmpt3rab1  6435  limomss  6604  unielxp  6735  f1o2ndf1  6807  smogt  6956  tfrlem1  6963  oawordeulem  7121  omass  7147  ecopovtrn  7332  php  7620  unxpdom  7643  findcard2d  7677  findcard3  7678  isfinite2  7693  fsuppimp  7750  fsuppunfi  7764  fsuppunbi  7765  fsuppres  7769  cantnfval2  8001  cantnfle  8003  cantnfp1lem3  8012  cantnflem1  8021  cantnfval2OLD  8031  cantnfleOLD  8033  cantnfp1lem3OLD  8038  cantnflem1OLD  8044  cnfcom  8057  cnfcomOLD  8065  rankr1ai  8129  rankonidlem  8159  rankxplim2  8211  oncard  8254  ficardom  8255  cardne  8259  acnnum  8346  alephord2i  8371  cardaleph  8383  aceq3lem  8414  dfac5lem5  8421  dfac12lem3  8438  cdainf  8485  ackbij1lem16  8528  cfslb  8559  cfslb2n  8561  cfsmolem  8563  fin4i  8591  infpssr  8601  fin1a2lem6  8698  axdc3lem2  8744  axcclem  8750  ttukeylem6  8807  fodomb  8817  gchi  8913  fpwwe2lem5  8923  pwfseqlem4  8951  pwfseq  8953  inawina  8979  wunfi  9010  inar1  9064  ltexnq  9264  ltbtwnnq  9267  ltexprlem4  9328  ltexpri  9332  prlem936  9336  suplem1pr  9341  suplem2pr  9342  recexsrlem  9391  mulgt0sr  9393  map2psrpr  9398  supsr  9400  eqlei  9605  eqlei2  9606  ledivp1i  10387  nnind  10470  nnmulcl  10475  nn0ge2m1nn  10778  nnnegz  10784  ublbneg  11085  xmulasslem  11398  ixxssixx  11464  iccshftri  11576  iccshftli  11578  iccdili  11580  icccntri  11582  1fv  11714  fzo1fzo0n0  11759  elfzonlteqm1  11790  ssfzo12  11804  zmodidfzoimp  11927  mptnn0fsuppr  12008  seqp1  12025  seqcl2  12028  seqfveq2  12032  seqshft2  12036  monoord  12040  seqsplit  12043  seqcaopr3  12045  seqf1olem2a  12048  seqf1o  12051  seqid2  12056  seqhomo  12057  hashf1rn  12327  hashinfxadd  12356  hashle00  12369  hashf1lem2  12409  seqcoll  12416  hash2pr  12419  pr2pwpr  12424  hash3tr  12433  brfi1uzind  12436  snopiswrd  12463  elovmptnn0wrd  12492  swrdswrd  12596  swrdccatin12lem2a  12621  swrdccat  12629  swrdccatin1d  12635  swrdccatin2d  12636  swrdccatin12d  12637  repswccat  12668  cshwidxmod  12685  relexpsucnnr  12862  rtrclreclem3  12895  rtrclreclem4  12896  dfrtrcl2  12897  relexpindlem  12898  relexpind  12899  rtrclind  12900  cjre  12974  climeu  13380  climub  13486  fsum2d  13588  fsumabs  13617  fsumrlim  13627  fsumo1  13628  fsumiun  13637  prodfn0  13705  prodfrec  13706  ntrivcvg  13708  fprodabs  13780  fprod2d  13787  fprodefsum  13832  ruclem9  13973  sadcadd  14110  sadadd2  14112  saddisjlem  14116  smuval2  14134  smupval  14140  smueqlem  14142  smumullem  14144  exprmfct  14253  eulerthlem2  14314  pcmpt  14413  vdwlem10  14510  cshwsidrepsw  14580  cshwshashlem1  14582  prmlem1a  14594  ressval3d  14698  mreexexd  15055  letsr  15974  pmtrfrn  16600  pmtr3ncom  16617  gsmtrcl  16658  psgnsn  16662  sylow1lem1  16735  efginvrel2  16862  efgsrel  16869  cntzcmnss  16966  gsumzoppg  17083  gsum2dlem2  17112  gsum2dOLD  17114  telgsumfzs  17131  dprdval  17147  dprdvalOLD  17149  ablfac1eulem  17236  pgpfac1  17244  pgpfac  17248  srgpcomp  17296  ring1ne0  17352  rimf1o  17496  rimrhm  17497  brric2  17507  0ringnnzr  18030  mplcoe1  18240  mplcoe3  18241  mplcoe3OLD  18242  mplcoe5lem  18243  mplcoe5  18244  mplcoe2OLD  18246  mpfaddcl  18316  mpfmulcl  18317  coe1ae0  18370  coe1fzgsumd  18457  gsummoncoe1  18459  pf1addcl  18502  pf1mulcl  18503  evl1gsumd  18506  zrhpsgnelbas  18721  psgndiflemA  18728  mamufacex  18976  mat0dimcrng  19057  mavmulsolcl  19138  mdetunilem9  19207  cramerlem3  19276  pmatcollpw3fi1  19374  pm2mpfo  19400  chmaidscmat  19434  chfacfscmul0  19444  chfacfpmmul0  19448  cpmadugsumlemF  19462  tg2  19551  neindisj2  19710  neiptopnei  19719  t1t0  19935  fiuncmp  19990  hmeof1o  20350  ist1-5lem  20406  t1r0  20407  alexsublem  20629  imasdsf1olem  20961  tgioo  21386  fsumcn  21459  voliunlem3  22047  itgfsum  22318  dvbsss  22391  dvmptfsum  22461  dvfsumlem2  22513  dvfsumlem4  22515  plyco  22723  dgrcolem1  22755  dgrco  22757  dvntaylp  22851  taylthlem1  22853  jensen  23435  bposlem5  23680  lgsquad2lem2  23751  dchrisum0flb  23812  pntpbnd1  23888  pntlemf  23907  brbtwn  24323  brcgr  24324  ushgrauhgra  24424  uhgra0v  24431  umisuhgra  24448  usgrac  24472  uslgraf1oedg  24480  uslisushgra  24484  uslisumgra  24485  usisuslgra  24486  elusuhgra  24489  usgra0v  24492  usgranloopv  24499  usgranloop  24500  usgra1v  24511  usgraidx2vlem2  24513  usgrafisindb0  24529  usgrafisindb1  24530  usgrafisinds  24534  usgrafisbase  24535  iscusgra0  24578  cusgrasize2inds  24598  cusgrafi  24603  2mwlk  24642  iswlkg  24645  wlkcpr  24650  edgwlk  24652  trliswlk  24662  2trllemE  24676  usgrnloop  24686  pthistrl  24695  spthispth  24696  pthdepisspth  24697  redwlk  24729  wlkdvspth  24731  usgra2adedgspthlem2  24733  usgra2wlkspth  24742  crctistrl  24749  cyclispth  24750  cycliscrct  24751  cyclnspth  24752  cyclispthon  24754  fargshiftf  24757  fargshiftf1  24758  fargshiftfo  24759  usgrcyclnl1  24761  usgrcyclnl2  24762  nvnencycllem  24764  3v3e3cycl1  24765  constr3trllem5  24775  constr3trl  24780  constr3pth  24781  constr3cycl  24782  4cycl4v4e  24787  4cycl4dv4e  24789  cusconngra  24797  wwlknimp  24808  wwlkn0  24810  wlkiswwlk1  24811  wlkiswwlk2lem4  24815  wlkiswwlk2  24818  wlklniswwlkn2  24821  wwlkiswwlkn  24823  2wlkeq  24828  wwlknred  24844  wwlknext  24845  wwlknextbi  24846  wwlknredwwlkn0  24848  wwlkextwrd  24849  wwlkm1edg  24856  wwlkextproplem3  24864  isclwlkg  24876  clwlkswlks  24879  clwwlkprop  24891  clwwlkgt0  24892  clwwlknimp  24897  clwlkisclwwlklem2a  24906  clwlkisclwwlklem1  24908  clwwlkext2edg  24923  clwwisshclww  24928  clwwnisshclwwn  24930  usghashecclwwlk  24956  wlklenvclwlk  24960  2spontn0vne  25008  usg2spthonot  25009  usg2spthonot0  25010  usgfidegfi  25031  usgravd00  25040  rgraprop  25049  rusgraprop  25050  rusgrargra  25051  cusgraisrusgra  25059  0eusgraiff0rgracl  25062  rusgrasn  25066  rusgranumwlklem1  25070  eupatrl  25089  eupath2  25101  3vfriswmgra  25126  3cyclfrgrarn1  25133  3cyclfrgrarn  25134  n4cyclfrgra  25139  frgranbnb  25141  frconngra  25142  vdfrgra0  25143  vdn0frgrav2  25144  vdgn0frgrav2  25145  usgn0fidegnn0  25150  frgrancvvdeqlem4  25154  frgrancvvdeqlem7  25157  frgrancvvdeqlemA  25158  frgrancvvdeqlemB  25159  frgrawopreglem4  25168  frgrawopreglem5  25169  frgrawopreg  25170  frgraregorufr0  25173  frgraeu  25175  frg2wot1  25178  frg2woteqm  25180  frg2woteq  25181  frgregordn0  25191  numclwwlkun  25200  numclwwlk8  25236  frgrareggt1  25237  frgrareg  25238  frgraregord013  25239  frgraregord13  25240  frgraogt3nreg  25241  friendshipgt3  25242  friendship  25243  opidon2OLD  25443  isexid2  25444  grpomndo  25465  elghomlem2OLD  25481  rngoidmlem  25542  rngoueqz  25549  blocn2  25840  cvexchlem  27403  cdj3lem2b  27472  cnvoprab  27696  nnindf  27763  issgon  28272  sitgclg  28467  sseqp1  28517  subfacp1lem6  28818  cvmliftlem7  28925  cvmliftlem10  28928  mclsrcl  29110  pprodss4v  29687  segleantisym  29918  rankeq1o  29981  mblfinlem3  30218  mbfresfi  30226  mettrifi  30416  iscringd  30562  mzpadd  30836  mzpmul  30837  mzpcompact2  30850  dford3lem2  31135  aomclem6  31171  cnsrexpcl  31282  lcmgcdlem  31380  nzin  31391  axc11next  31481  iotavalsb  31508  fperiodmullem  31669  fmul01  31740  fmulcl  31741  fmuldfeqlem1  31742  fmuldfeq  31743  iblspltprt  31938  itgspltprt  31944  stoweidlem2  31950  stoweidlem3  31951  stoweidlem6  31954  stoweidlem8  31956  stoweidlem17  31965  stoweidlem19  31967  stoweidlem21  31969  stoweidlem26  31974  stoweidlem31  31979  stoweidlem43  31991  fourierdlem42  32097  eu2ndop1stv  32373  funressnfv  32379  afv0fv0  32400  afv0nbfvbi  32402  mod2eq1n2dvds  32462  ssfz12  32651  fzoopth  32660  usgra2pthspth  32669  spthdifv  32670  usgra2pth  32672  uhgrasiz  32712  usgfis  32764  usgfisALT  32768  clcllaw  32833  intop  32845  clintop  32850  assintop  32851  assintopcllaw  32854  lmod0rng  32874  ringrng  32885  rngimf1o  32911  rngimrnghm  32912  ztprmneprm  33136  scmsuppss  33165  ply1mulgsumlem1  33186  ply1mulgsumlem2  33187  lcoel0  33229  ellcoellss  33236  lindslinindsimp2lem5  33263  ldepspr  33274  nno  33338  nn0o  33339  flnn0div2ge  33350  nnolog2flm1  33411  blengt1fldiv2p1  33414  dignn0flhalf  33439  bnj938  34342  bnj964  34348  bnj1052  34378  bnj1125  34395  cdlemk35s  37076  cdlemk39s  37078  cdlemk42  37080  iunrelexpmin1  38225  iunrelexpmin2  38226  relexpss1d  38235
  Copyright terms: Public domain W3C validator