Theorem mpd 13

Description: A modus ponens deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpd.1	⊢ (𝜑 → 𝜓)
mpd.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mpd	⊢ (𝜑 → 𝜒)

Proof of Theorem mpd

Step	Hyp	Ref	Expression
1		mpd.1	. 2 ⊢ (𝜑 → 𝜓)
2		mpd.2	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	a2i 11	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
4	1, 3	ax-mp 5	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-2 7

This theorem is referenced by:  syl  14  mpi  15  id  19  mpcom  36  mpdd  41  mp2d  47  pm2.43i  49  syl3c  63  mpbid  147  mpbird  167  jcai  311  mp2and  437  pm2.21dd  629  mt2d  634  mpnanrd  704  mpjaod  730  stdcndcOLD  858  impidc  870  jadc  875  pm2.54dc  903  oplem1  988  mp3and  1381  xor3dc  1436  exlimdd  1925  exlimddv  1954  eqrdav  2237  necon1aidc  2471  necon1bidc  2472  necon4aidc  2488  reximddv  2653  reximssdv  2654  rexlimddv  2673  vtoclgft  2873  rspcedvd  2935  sseldd  3249  ssneldd  3251  tpid3g  3826  preq12b  3893  axpweq  4306  exmid1dc  4335  exmid1stab  4343  opth  4375  issod  4462  frirrg  4493  frind  4495  ralxfr2d  4608  rexxfr2d  4609  eldifpw  4621  onun2  4635  onuni  4639  elirr  4686  en2lp  4699  wetriext  4722  peano2  4740  relop  4928  elres  5097  sotri2  5183  iota4an  5356  iota5  5357  funeu  5400  funopg  5409  imadiflem  5458  funimaexglem  5462  ssimaex  5761  ffvelcdm  5835  dff3im  5847  dffo4  5850  funopsn  5885  f1eqcocnv  5991  f1oiso2  6027  riota5f  6059  riotass2  6061  acexmidlemcase  6074  elovimad  6123  ovmpodf  6214  ovmpodv2  6216  ovi3  6220  ov6g  6221  caoftrn  6329  op1steq  6407  fvdifsuppst  6478  suppssdc  6494  suppofss1dcl  6498  suppofss2dcl  6499  tfr0dm  6587  tfrlemibxssdm  6592  tfrlemi14d  6598  tfr1onlembxssdm  6608  tfr1onlemaccex  6613  tfr1onlemres  6614  tfrcllembxssdm  6621  tfrcllemaccex  6626  tfrcllemres  6627  rdgivallem  6646  nnsucelsuc  6758  nnsucsssuc  6759  dcdifsnid  6771  nnawordex  6796  ersym  6813  mapvalg  6926  pmvalg  6927  mapsnd  6964  mapsn  6966  fundmen  7088  1dom1el  7101  en2  7106  pw2f1odclem  7128  mapdom1g  7141  fidceq  7165  fin0or  7184  findcard2  7187  findcard2s  7188  fidcen  7197  prfidceq  7229  fiintim  7232  suplub2ti  7335  supsnti  7339  supisoex  7343  difinfsnlem  7433  difinfsn  7434  ctm  7443  ctssdclemn0  7444  ctssdccl  7445  ctssdc  7447  enumctlemm  7448  nninfninc  7457  nnnninfeq2  7463  enomnilem  7472  exmidomniim  7475  exmidomni  7476  fodjuomnilemdc  7478  fodjuomnilemres  7482  omnimkv  7490  mkvprop  7492  omniwomnimkv  7501  en2prde  7533  pr2cv1  7535  en2eleq  7541  acfun  7557  exmidontriimlem1  7571  exmidontriimlem4  7574  exmidontriim  7575  papsym  7606  papcotr  7607  ccfunen  7624  cc4f  7629  cc4n  7631  elni2  7675  mulclpi  7689  nlt1pig  7702  indpi  7703  recclnq  7753  ltexnqq  7769  halfnqq  7771  prarloclemarch  7779  prarloclemarch2  7780  prop  7836  prltlu  7848  prarloclem3step  7857  prarloclem5  7861  prarloclem  7862  prarloc  7864  prarloc2  7865  genpml  7878  genpmu  7879  genprndl  7882  genprndu  7883  genpdisj  7884  addnqprllem  7888  addnqprulem  7889  addlocprlemeq  7894  addlocprlemgt  7895  addlocprlem  7896  addlocpr  7897  nqprloc  7906  nqprl  7912  nqpru  7913  addnqprlemrl  7918  addnqprlemru  7919  appdivnq  7924  prmuloc  7927  prmuloc2  7928  mullocprlem  7931  mullocpr  7932  mulnqprlemrl  7934  mulnqprlemru  7935  ltprordil  7950  ltpopr  7956  ltsopr  7957  ltaddpr  7958  ltexprlemm  7961  ltexprlemopl  7962  ltexprlemlol  7963  ltexprlemopu  7964  ltexprlemupu  7965  ltexprlemloc  7968  ltexprlemfl  7970  ltexprlemrl  7971  ltexprlemfu  7972  ltexprlemru  7973  ltaprg  7980  recexprlemm  7985  recexprlem1ssl  7994  recexprlem1ssu  7995  aptiprleml  8000  aptiprlemu  8001  archpr  8004  cauappcvgprlemm  8006  cauappcvgprlemopl  8007  cauappcvgprlemlol  8008  cauappcvgprlemopu  8009  cauappcvgprlemupu  8010  cauappcvgprlemdisj  8012  cauappcvgprlemloc  8013  cauappcvgprlemladdfu  8015  cauappcvgprlemladdfl  8016  cauappcvgprlemladdru  8017  cauappcvgprlem1  8020  archrecpr  8025  caucvgprlemnkj  8027  caucvgprlemnbj  8028  caucvgprlemm  8029  caucvgprlemopl  8030  caucvgprlemlol  8031  caucvgprlemopu  8032  caucvgprlemupu  8033  caucvgprlemdisj  8035  caucvgprlemloc  8036  caucvgprlemladdfu  8038  caucvgprlem1  8040  caucvgprlemlim  8042  caucvgprprlemnbj  8054  caucvgprprlemml  8055  caucvgprprlemopl  8058  caucvgprprlemlol  8059  caucvgprprlemopu  8060  caucvgprprlemupu  8061  caucvgprprlemdisj  8063  caucvgprprlemloc  8064  caucvgprprlemexbt  8067  caucvgprprlemaddq  8069  caucvgprprlemlim  8072  suplocexprlemss  8076  suplocexprlemrl  8078  suplocexprlemmu  8079  suplocexprlemru  8080  suplocexprlemdisj  8081  suplocexprlemloc  8082  suplocexprlemub  8084  suplocexprlemlub  8085  recexgt0sr  8134  mulgt0sr  8139  archsr  8143  caucvgsrlemoffcau  8159  suplocsrlemb  8167  suplocsrlempr  8168  suplocsrlem  8169  cnm  8193  axarch  8252  axcaucvglemcau  8259  axpre-suploclemres  8262  lelttr  8408  ltletr  8409  ltled  8439  cnegexlem1  8495  cnegexlem2  8496  renegcl  8581  negf1o  8703  gt0add  8895  apreap  8909  apirr  8927  apsym  8928  apcotr  8929  apadd1  8930  apneg  8933  mulext1  8934  mulap0r  8937  apti  8944  aprcl  8968  aptap  8972  recexap  8975  mulap0  8976  receuap  8993  mul0eqap  8994  lep1  9169  lem1  9171  letrp1  9172  recreclt  9224  lbinf  9272  suprubex  9275  nnrecgt0  9325  bndndx  9545  nn0ge2m1nn  9610  elnn0z  9640  peano2z  9663  zaddcl  9667  ztri3or0  9669  zltnle  9673  zdceq  9703  zdcle  9704  zdclt  9705  zdiv  9717  zeo  9734  fnn0ind  9745  btwnz  9748  uzm1  9936  uzp1  9939  indstr  9976  supinfneg  9978  infsupneg  9979  eluzdc  9993  nn01to3  10000  qapne  10022  xrltled  10184  xrlelttr  10191  xrltletr  10192  ge0nemnf  10209  fzdcel  10427  elfzouz2  10552  fzoss1  10563  fzospliti  10568  elincfzoext  10594  fzocatel  10600  fzostep1  10639  zsupcllemstep  10645  zsupcl  10647  infssuzledc  10650  qtri3or  10658  qltnle  10661  qdceq  10662  qdclt  10663  exbtwnzlemex  10667  rebtwn2zlemstep  10670  rebtwn2z  10672  qbtwnxr  10675  ioom  10678  ico0  10679  ioc0  10680  flqeqceilz  10738  modqadd1  10781  modqmul1  10797  frec2uzuzd  10822  frec2uzlt2d  10824  frec2uzf1od  10826  frecuzrdgrrn  10828  frec2uzrdg  10829  frecuzrdgrcl  10830  frecuzrdgsuc  10834  frecuzrdgrclt  10835  frecuzrdgdomlem  10837  uzsinds  10864  seqvalcd  10881  seqovcd  10887  seq3fveq2  10895  seqfveq2g  10897  seq3shft2  10901  seqshft2g  10902  monoord  10905  seq3split  10908  seqsplitg  10909  seq3caopr3  10911  iseqf1olemab  10922  iseqf1olemnanb  10923  iseqf1olemqk  10927  seqf1oglem1  10939  seqf1og  10941  seq3id3  10944  seq3id2  10946  seq3homo  10947  seqhomog  10950  expgt1  10997  m1expeven  11006  expnbnd  11084  expnlbnd2  11086  nn0ltexp2  11130  apexp1  11139  hashennn  11202  hashfibclem  11265  hashf1lem2  11269  zfz1isolem1  11275  seq3coll  11277  pfxwrdsymbg  11445  wrdind  11477  wrd2ind  11478  cjap  11655  caucvgre  11730  cvg1nlemres  11734  resqrexlemgt0  11769  resqrexlemglsq  11771  resqrexlemga  11772  resqrtcl  11778  abslt  11837  abssubap0  11839  abssubne0  11840  caubnd2  11866  qdenre  11951  maxabslemlub  11956  maxabs  11958  maxleast  11962  fimaxre2  11976  xrmaxiflemlub  11997  xrmaxif  12000  xrmaxltsup  12007  xrmaxadd  12010  xrmineqinf  12018  climuni  12042  2clim  12050  climcn1  12057  climcn2  12058  subcn2  12060  mulcn2  12061  climsqz  12084  climsqz2  12085  climcau  12096  climcvg1nlem  12098  climcaucn  12100  serf0  12101  sumrbdclem  12127  summodclem2  12132  zsumdc  12134  divcnv  12247  absltap  12259  absgtap  12260  mertenslem2  12286  ntrivcvgap  12298  prodrbdclem  12321  prodmodclem2  12327  zproddc  12329  prodssdc  12339  fprodsplitdc  12346  fprodcl2lem  12355  efcllemp  12408  tanvalap  12458  sin01bnd  12507  cos01bnd  12508  sin01gt0  12512  absef  12520  eirrap  12528  dvds0  12556  dvdsmul1  12563  dvdsmultr1d  12582  dvdslelemd  12593  divconjdvds  12599  alzdvds  12604  3dvds  12614  sqoddm1div8z  12636  nno  12656  divalglemex  12672  bits0o  12700  dvdsbnd  12716  dvdslegcd  12724  zeqzmulgcd  12730  gcd0id  12739  gcdaddm  12744  gcd1  12747  gcdabs  12748  bezoutlemnewy  12756  bezoutlemstep  12757  bezoutlemmain  12758  bezoutlemex  12761  bezoutlemzz  12762  bezoutlemaz  12763  bezoutlembz  12764  bezoutlembi  12765  bezoutlemle  12768  bezoutlemsup  12769  mulgcd  12776  gcdzeq  12782  dvdsmulgcd  12785  sqgcd  12789  bezoutr1  12793  nninfctlemfo  12800  algcvga  12812  algfx  12813  eucalglt  12818  eucalg  12820  lcmneg  12835  lcmabs  12837  lcmgcdlem  12838  ncoprmgcdne1b  12850  mulgcddvds  12855  qredeq  12857  divgcdcoprm0  12862  cncongr1  12864  isprm2lem  12877  nprm  12884  dvdsnprmd  12886  prmdvdsfz  12900  isprm5lem  12902  coprm  12905  isprm6  12908  sqrt2irr  12923  pw2dvdslemn  12926  pw2dvdseulemle  12928  oddpwdclemdvds  12931  oddpwdclemndvds  12932  sqrt2irrap  12941  qnumdencl  12948  prmdiv  12996  modprmn0modprm0  13018  prm23lt5  13025  pythagtriplem4  13030  pythagtriplem19  13044  pythagtrip  13045  pclemub  13049  pcpre1  13054  pcpremul  13055  pceulem  13056  pcqcl  13068  pcidlem  13085  pcgcd1  13090  pc2dvds  13092  dvdsprmpweqle  13099  difsqpwdvds  13100  pcadd  13102  pcmpt  13105  expnprm  13115  pockthg  13119  infpnlem2  13122  prmunb  13124  1arith  13129  4sqlem10  13149  4sqlem11  13163  4sqlem12  13164  4sqlem13m  13165  4sqlem17  13169  4sqlem18  13170  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemfrceq  13255  ennnfonelemex  13288  ennnfonelemhom  13289  ennnfonelemrnh  13290  ennnfonelemnn0  13296  ennnfonelemim  13298  exmidunben  13300  ctinfomlemom  13301  ctinfom  13302  ctinf  13304  omctfn  13317  nninfdclemp1  13324  setscomd  13376  imasaddfnlemg  13618  mhmf1o  13760  grpinveu  13826  grpasscan1  13851  dfgrp3mlem  13886  grp1inv  13895  issubg4m  13979  ghmf1o  14061  srgisid  14273  ringadd2  14315  ringinvnzdiv  14338  unitgrp  14406  ringelnzr  14477  lringuplu  14486  subrguss  14527  subrgintm  14534  aprcotr  14580  islmodd  14612  lssclg  14684  lss0cl  14689  lssvneln0  14693  lss1d  14703  lmodindp1  14748  rnglidlmmgm  14816  znidomb  14976  znunit  14977  znrrg  14978  rnasclassa  15021  mplsubgfilemcl  15073  mplsubgfileminv  15074  tgcl  15148  neii1  15231  neii2  15233  neiss  15234  tpnei  15244  tgrest  15253  ssrest  15266  icnpimaex  15295  lmcvg  15301  cnpnei  15303  cnptopco  15306  lmff  15333  txcnp  15355  txcn  15359  hmeontr  15397  blssec  15522  mopni3  15568  blsscls2  15577  comet  15583  bdxmet  15585  bdmopn  15588  xmettxlem  15593  xmettx  15594  addcncntoplem  15645  mpomulcn  15650  mulc1cncf  15673  cncfco  15675  cncfmptc  15680  mulcncflem  15691  mulcncf  15692  dedekindeulemlu  15705  dedekindeulemeu  15706  suplociccreex  15708  suplociccex  15709  dedekindicclemlu  15714  dedekindicclemeu  15715  ivthinclemlopn  15720  ivthinclemlr  15721  ivthinclemuopn  15722  ivthinclemur  15723  ivthinclemloc  15725  ivthinc  15727  ivthreinc  15729  ivthdichlem  15735  limcimolemlt  15748  limcresi  15750  cnplimcim  15751  cnplimclemle  15752  cnplimclemr  15753  limccnpcntop  15759  limccoap  15762  dvcoapbr  15791  dvcj  15793  plyf  15821  plyaddlem1  15831  plymullem1  15832  plyco  15843  plycj  15845  plycn  15846  plyrecj  15847  dvply2g  15850  efltlemlt  15858  sin0pilem2  15866  tangtx  15922  logdivlti  15965  rplogbval  16030  logbgcd1irraplemexp  16053  logbgcd1irraplemap  16054  logbgcd1irrap  16055  birthdaylem1g  16070  perfect1  16095  perfectlem1  16096  perfectlem2  16097  lgsval4a  16124  lgsdir2lem3  16132  lgsne0  16140  gausslemma2dlem3  16165  gausslemma2dlem4  16166  gausslemma2dlem6  16169  gausslemma2dlem7  16170  gausslemma2d  16171  lgseisenlem1  16172  lgsquadlem2  16180  lgsquadlem3  16181  lgsquad2lem2  16184  lgsquad3  16186  2lgsoddprmlem2  16208  2sqlem8a  16224  2sqlem8  16225  2sqlem9  16226  lpvtx  16303  upgrex  16327  upgr1een  16348  edgupgren  16365  umgredg  16369  upgrpredgv  16370  upgredg2vtx  16372  upgredgpr  16373  uspgrf1oedg  16400  usgredg4  16439  uspgredgdomord  16453  usgr1vr  16472  wlkvtxiedg  16569  wlkvtxiedgg  16570  wlk1walkdom  16583  upgriswlkdc  16584  upgrwlkedg  16585  uspgr2wlkeq  16589  uspgr2wlkeqi  16591  umgrwlknloop  16592  eupth2lem2dc  16683  trlsegvdeglem1  16684  eupth2lem3lem4fi  16697  bj-exlimmpi  16781  uzdcinzz  16809  bj-charfundcALT  16818  bj-2inf  16947  bj-peano4  16964  bj-nn0suc  16973  pw1ndom3  17003  subctctexmid  17013  exmidcon  17019  nninfalllem1  17025  nninfsellemqall  17032  nninfomnilem  17035  nninffeq  17037  nnnninfex  17039  exmidsbthrlem  17041  sbthomlem  17044  refeq  17047  isomninnlem  17053  apdifflemr  17070  redcwlpo  17079  reap0  17082  nconstwlpolem  17089