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  433  pm2.21dd  620  mt2d  625  mpjaod  718  stdcndcOLD  846  impidc  858  jadc  863  pm2.54dc  891  pm4.55dc  938  oplem1  975  mp3and  1340  xor3dc  1387  exlimdd  1872  exlimddv  1898  eqrdav  2176  necon1aidc  2398  necon1bidc  2399  necon4aidc  2415  reximddv  2580  reximssdv  2581  rexlimddv  2599  vtoclgft  2787  rspcedvd  2847  sseldd  3156  ssneldd  3158  tpid3g  3707  preq12b  3770  axpweq  4171  exmid1dc  4200  exmid1stab  4208  opth  4237  issod  4319  frirrg  4350  frind  4352  ralxfr2d  4464  rexxfr2d  4465  eldifpw  4477  onun2  4489  onuni  4493  elirr  4540  en2lp  4553  wetriext  4576  peano2  4594  relop  4777  elres  4943  sotri2  5026  iota4an  5197  iota5  5198  funeu  5241  funopg  5250  imadiflem  5295  funimaexglem  5299  ssimaex  5577  ffvelcdm  5649  dff3im  5661  dffo4  5664  f1eqcocnv  5791  f1oiso2  5827  riota5f  5854  riotass2  5856  acexmidlemcase  5869  ovmpodf  6005  ovmpodv2  6007  ovi3  6010  ov6g  6011  caoftrn  6107  op1steq  6179  tfr0dm  6322  tfrlemibxssdm  6327  tfrlemi14d  6333  tfr1onlembxssdm  6343  tfr1onlemaccex  6348  tfr1onlemres  6349  tfrcllembxssdm  6356  tfrcllemaccex  6361  tfrcllemres  6362  rdgivallem  6381  nnsucelsuc  6491  nnsucsssuc  6492  dcdifsnid  6504  nnawordex  6529  ersym  6546  mapvalg  6657  pmvalg  6658  mapsn  6689  fundmen  6805  mapdom1g  6846  fidceq  6868  fin0or  6885  findcard2  6888  findcard2s  6889  fiintim  6927  suplub2ti  6999  supsnti  7003  supisoex  7007  difinfsnlem  7097  difinfsn  7098  ctm  7107  ctssdclemn0  7108  ctssdccl  7109  ctssdc  7111  enumctlemm  7112  nnnninfeq2  7126  enomnilem  7135  exmidomniim  7138  exmidomni  7139  fodjuomnilemdc  7141  fodjuomnilemres  7145  omnimkv  7153  mkvprop  7155  omniwomnimkv  7164  en2eleq  7193  acfun  7205  exmidontriimlem1  7219  exmidontriimlem4  7222  exmidontriim  7223  ccfunen  7262  cc4f  7267  cc4n  7269  elni2  7312  mulclpi  7326  nlt1pig  7339  indpi  7340  recclnq  7390  ltexnqq  7406  halfnqq  7408  prarloclemarch  7416  prarloclemarch2  7417  prop  7473  prltlu  7485  prarloclem3step  7494  prarloclem5  7498  prarloclem  7499  prarloc  7501  prarloc2  7502  genpml  7515  genpmu  7516  genprndl  7519  genprndu  7520  genpdisj  7521  addnqprllem  7525  addnqprulem  7526  addlocprlemeq  7531  addlocprlemgt  7532  addlocprlem  7533  addlocpr  7534  nqprloc  7543  nqprl  7549  nqpru  7550  addnqprlemrl  7555  addnqprlemru  7556  appdivnq  7561  prmuloc  7564  prmuloc2  7565  mullocprlem  7568  mullocpr  7569  mulnqprlemrl  7571  mulnqprlemru  7572  ltprordil  7587  ltpopr  7593  ltsopr  7594  ltaddpr  7595  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemlol  7600  ltexprlemopu  7601  ltexprlemupu  7602  ltexprlemloc  7605  ltexprlemfl  7607  ltexprlemrl  7608  ltexprlemfu  7609  ltexprlemru  7610  ltaprg  7617  recexprlemm  7622  recexprlem1ssl  7631  recexprlem1ssu  7632  aptiprleml  7637  aptiprlemu  7638  archpr  7641  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemopu  7646  cauappcvgprlemupu  7647  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlemladdru  7654  cauappcvgprlem1  7657  archrecpr  7662  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemopu  7669  caucvgprlemupu  7670  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemladdfu  7675  caucvgprlem1  7677  caucvgprlemlim  7679  caucvgprprlemnbj  7691  caucvgprprlemml  7692  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemupu  7698  caucvgprprlemdisj  7700  caucvgprprlemloc  7701  caucvgprprlemexbt  7704  caucvgprprlemaddq  7706  caucvgprprlemlim  7709  suplocexprlemss  7713  suplocexprlemrl  7715  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemub  7721  suplocexprlemlub  7722  recexgt0sr  7771  mulgt0sr  7776  archsr  7780  caucvgsrlemoffcau  7796  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  cnm  7830  axarch  7889  axcaucvglemcau  7896  axpre-suploclemres  7899  lelttr  8045  ltletr  8046  ltled  8075  cnegexlem1  8131  cnegexlem2  8132  renegcl  8217  negf1o  8338  gt0add  8529  apreap  8543  apirr  8561  apsym  8562  apcotr  8563  apadd1  8564  apneg  8567  mulext1  8568  mulap0r  8571  apti  8578  aprcl  8602  aptap  8606  recexap  8609  mulap0  8610  receuap  8625  mul0eqap  8626  lep1  8801  lem1  8803  letrp1  8804  recreclt  8856  lbinf  8904  suprubex  8907  nnrecgt0  8956  bndndx  9174  nn0ge2m1nn  9235  elnn0z  9265  peano2z  9288  zaddcl  9292  ztri3or0  9294  zltnle  9298  zdceq  9327  zdcle  9328  zdclt  9329  zdiv  9340  zeo  9357  fnn0ind  9368  btwnz  9371  uzm1  9557  uzp1  9560  indstr  9592  supinfneg  9594  infsupneg  9595  eluzdc  9609  nn01to3  9616  qapne  9638  xrltled  9798  xrlelttr  9805  xrltletr  9806  ge0nemnf  9823  fzdcel  10039  elfzouz2  10160  fzoss1  10170  fzospliti  10175  fzocatel  10198  fzostep1  10236  qtri3or  10242  qltnle  10245  qdceq  10246  exbtwnzlemex  10249  rebtwn2zlemstep  10252  rebtwn2z  10254  qbtwnxr  10257  ioom  10260  ico0  10261  ioc0  10262  flqeqceilz  10317  modqadd1  10360  modqmul1  10376  frec2uzuzd  10401  frec2uzlt2d  10403  frec2uzf1od  10405  frecuzrdgrrn  10407  frec2uzrdg  10408  frecuzrdgrcl  10409  frecuzrdgsuc  10413  frecuzrdgrclt  10414  frecuzrdgdomlem  10416  uzsinds  10441  seqvalcd  10458  seqovcd  10462  seq3fveq2  10468  seq3shft2  10472  monoord  10475  seq3split  10478  seq3caopr3  10480  iseqf1olemab  10488  iseqf1olemnanb  10489  iseqf1olemqk  10493  seq3id3  10506  seq3id2  10508  seq3homo  10509  expgt1  10557  m1expeven  10566  expnbnd  10643  expnlbnd2  10645  nn0ltexp2  10688  apexp1  10697  hashennn  10759  zfz1isolem1  10819  seq3coll  10821  cjap  10914  caucvgre  10989  cvg1nlemres  10993  resqrexlemgt0  11028  resqrexlemglsq  11030  resqrexlemga  11031  resqrtcl  11037  abslt  11096  abssubap0  11098  abssubne0  11099  caubnd2  11125  qdenre  11210  maxabslemlub  11215  maxabs  11217  maxleast  11221  fimaxre2  11234  xrmaxiflemlub  11255  xrmaxif  11258  xrmaxltsup  11265  xrmaxadd  11268  xrmineqinf  11276  climuni  11300  2clim  11308  climcn1  11315  climcn2  11316  subcn2  11318  mulcn2  11319  climsqz  11342  climsqz2  11343  climcau  11354  climcvg1nlem  11356  climcaucn  11358  serf0  11359  sumrbdclem  11384  summodclem2  11389  zsumdc  11391  divcnv  11504  absltap  11516  absgtap  11517  mertenslem2  11543  ntrivcvgap  11555  prodrbdclem  11578  prodmodclem2  11584  zproddc  11586  prodssdc  11596  fprodsplitdc  11603  fprodcl2lem  11612  efcllemp  11665  tanvalap  11715  sin01bnd  11764  cos01bnd  11765  sin01gt0  11768  absef  11776  eirrap  11784  dvds0  11812  dvdsmul1  11819  dvdsmultr1d  11838  dvdslelemd  11848  divconjdvds  11854  alzdvds  11859  sqoddm1div8z  11890  nno  11910  divalglemex  11926  zsupcllemstep  11945  zsupcl  11947  infssuzledc  11950  dvdsbnd  11956  dvdslegcd  11964  zeqzmulgcd  11970  gcd0id  11979  gcdaddm  11984  gcd1  11987  gcdabs  11988  bezoutlemnewy  11996  bezoutlemstep  11997  bezoutlemmain  11998  bezoutlemex  12001  bezoutlemzz  12002  bezoutlemaz  12003  bezoutlembz  12004  bezoutlembi  12005  bezoutlemle  12008  bezoutlemsup  12009  mulgcd  12016  gcdzeq  12022  dvdsmulgcd  12025  sqgcd  12029  bezoutr1  12033  algcvga  12050  algfx  12051  eucalglt  12056  eucalg  12058  lcmneg  12073  lcmabs  12075  lcmgcdlem  12076  ncoprmgcdne1b  12088  mulgcddvds  12093  qredeq  12095  divgcdcoprm0  12100  cncongr1  12102  isprm2lem  12115  nprm  12122  dvdsnprmd  12124  prmdvdsfz  12138  isprm5lem  12140  coprm  12143  isprm6  12146  sqrt2irr  12161  pw2dvdslemn  12164  pw2dvdseulemle  12166  oddpwdclemdvds  12169  oddpwdclemndvds  12170  sqrt2irrap  12179  qnumdencl  12186  prmdiv  12234  modprmn0modprm0  12255  prm23lt5  12262  pythagtriplem4  12267  pythagtriplem19  12281  pythagtrip  12282  pclemub  12286  pcpre1  12291  pcpremul  12292  pceulem  12293  pcqcl  12305  pcidlem  12321  pcgcd1  12326  pc2dvds  12328  dvdsprmpweqle  12335  difsqpwdvds  12336  pcadd  12338  pcmpt  12340  expnprm  12350  pockthg  12354  infpnlem2  12357  prmunb  12359  1arith  12364  4sqlem10  12384  ennnfonelemex  12414  ennnfonelemhom  12415  ennnfonelemrnh  12416  ennnfonelemnn0  12422  ennnfonelemim  12424  exmidunben  12426  ctinfomlemom  12427  ctinfom  12428  ctinf  12430  omctfn  12443  nninfdclemp1  12450  setscomd  12502  imasaddfnlemg  12734  mhmf1o  12860  grpinveu  12910  grpasscan1  12932  dfgrp3mlem  12967  grp1inv  12976  issubg4m  13051  srgisid  13167  ringadd2  13208  ringinvnzdiv  13225  unitgrp  13283  ringelnzr  13326  lringuplu  13335  subrguss  13355  subrgintm  13362  aprcotr  13373  islmodd  13381  tgcl  13534  neii1  13617  neii2  13619  neiss  13620  tpnei  13630  tgrest  13639  ssrest  13652  icnpimaex  13681  lmcvg  13687  cnpnei  13689  cnptopco  13692  lmff  13719  txcnp  13741  txcn  13745  hmeontr  13783  blssec  13908  mopni3  13954  blsscls2  13963  comet  13969  bdxmet  13971  bdmopn  13974  xmettxlem  13979  xmettx  13980  addcncntoplem  14021  mulc1cncf  14046  cncfco  14048  cncfmptc  14052  mulcncflem  14060  mulcncf  14061  dedekindeulemlu  14069  dedekindeulemeu  14070  suplociccreex  14072  suplociccex  14073  dedekindicclemlu  14078  dedekindicclemeu  14079  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemloc  14089  ivthinc  14091  limcimolemlt  14103  limcresi  14105  cnplimcim  14106  cnplimclemle  14107  cnplimclemr  14108  limccnpcntop  14114  limccoap  14117  dvcoapbr  14141  dvcj  14143  efltlemlt  14165  sin0pilem2  14173  tangtx  14229  logdivlti  14272  rplogbval  14333  logbgcd1irraplemexp  14356  logbgcd1irraplemap  14357  logbgcd1irrap  14358  lgsval4a  14393  lgsdir2lem3  14401  lgsne0  14409  lgseisenlem1  14420  2lgsoddprmlem2  14424  2sqlem8a  14439  2sqlem8  14440  2sqlem9  14441  bj-exlimmpi  14492  uzdcinzz  14520  bj-charfundcALT  14531  bj-2inf  14660  bj-peano4  14677  bj-nn0suc  14686  subctctexmid  14720  nninfalllem1  14727  nninfsellemqall  14734  nninfomnilem  14737  nninffeq  14739  exmidsbthrlem  14740  sbthomlem  14743  refeq  14746  isomninnlem  14748  apdifflemr  14765  redcwlpo  14773  reap0  14776  nconstwlpolem  14782