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  2789  rspcedvd  2849  sseldd  3158  ssneldd  3160  tpid3g  3709  preq12b  3772  axpweq  4173  exmid1dc  4202  exmid1stab  4210  opth  4239  issod  4321  frirrg  4352  frind  4354  ralxfr2d  4466  rexxfr2d  4467  eldifpw  4479  onun2  4491  onuni  4495  elirr  4542  en2lp  4555  wetriext  4578  peano2  4596  relop  4779  elres  4945  sotri2  5028  iota4an  5199  iota5  5200  funeu  5243  funopg  5252  imadiflem  5297  funimaexglem  5301  ssimaex  5580  ffvelcdm  5652  dff3im  5664  dffo4  5667  f1eqcocnv  5795  f1oiso2  5831  riota5f  5858  riotass2  5860  acexmidlemcase  5873  ovmpodf  6009  ovmpodv2  6011  ovi3  6014  ov6g  6015  caoftrn  6111  op1steq  6183  tfr0dm  6326  tfrlemibxssdm  6331  tfrlemi14d  6337  tfr1onlembxssdm  6347  tfr1onlemaccex  6352  tfr1onlemres  6353  tfrcllembxssdm  6360  tfrcllemaccex  6365  tfrcllemres  6366  rdgivallem  6385  nnsucelsuc  6495  nnsucsssuc  6496  dcdifsnid  6508  nnawordex  6533  ersym  6550  mapvalg  6661  pmvalg  6662  mapsn  6693  fundmen  6809  mapdom1g  6850  fidceq  6872  fin0or  6889  findcard2  6892  findcard2s  6893  fiintim  6931  suplub2ti  7003  supsnti  7007  supisoex  7011  difinfsnlem  7101  difinfsn  7102  ctm  7111  ctssdclemn0  7112  ctssdccl  7113  ctssdc  7115  enumctlemm  7116  nnnninfeq2  7130  enomnilem  7139  exmidomniim  7142  exmidomni  7143  fodjuomnilemdc  7145  fodjuomnilemres  7149  omnimkv  7157  mkvprop  7159  omniwomnimkv  7168  en2eleq  7197  acfun  7209  exmidontriimlem1  7223  exmidontriimlem4  7226  exmidontriim  7227  ccfunen  7266  cc4f  7271  cc4n  7273  elni2  7316  mulclpi  7330  nlt1pig  7343  indpi  7344  recclnq  7394  ltexnqq  7410  halfnqq  7412  prarloclemarch  7420  prarloclemarch2  7421  prop  7477  prltlu  7489  prarloclem3step  7498  prarloclem5  7502  prarloclem  7503  prarloc  7505  prarloc2  7506  genpml  7519  genpmu  7520  genprndl  7523  genprndu  7524  genpdisj  7525  addnqprllem  7529  addnqprulem  7530  addlocprlemeq  7535  addlocprlemgt  7536  addlocprlem  7537  addlocpr  7538  nqprloc  7547  nqprl  7553  nqpru  7554  addnqprlemrl  7559  addnqprlemru  7560  appdivnq  7565  prmuloc  7568  prmuloc2  7569  mullocprlem  7572  mullocpr  7573  mulnqprlemrl  7575  mulnqprlemru  7576  ltprordil  7591  ltpopr  7597  ltsopr  7598  ltaddpr  7599  ltexprlemm  7602  ltexprlemopl  7603  ltexprlemlol  7604  ltexprlemopu  7605  ltexprlemupu  7606  ltexprlemloc  7609  ltexprlemfl  7611  ltexprlemrl  7612  ltexprlemfu  7613  ltexprlemru  7614  ltaprg  7621  recexprlemm  7626  recexprlem1ssl  7635  recexprlem1ssu  7636  aptiprleml  7641  aptiprlemu  7642  archpr  7645  cauappcvgprlemm  7647  cauappcvgprlemopl  7648  cauappcvgprlemlol  7649  cauappcvgprlemopu  7650  cauappcvgprlemupu  7651  cauappcvgprlemdisj  7653  cauappcvgprlemloc  7654  cauappcvgprlemladdfu  7656  cauappcvgprlemladdfl  7657  cauappcvgprlemladdru  7658  cauappcvgprlem1  7661  archrecpr  7666  caucvgprlemnkj  7668  caucvgprlemnbj  7669  caucvgprlemm  7670  caucvgprlemopl  7671  caucvgprlemlol  7672  caucvgprlemopu  7673  caucvgprlemupu  7674  caucvgprlemdisj  7676  caucvgprlemloc  7677  caucvgprlemladdfu  7679  caucvgprlem1  7681  caucvgprlemlim  7683  caucvgprprlemnbj  7695  caucvgprprlemml  7696  caucvgprprlemopl  7699  caucvgprprlemlol  7700  caucvgprprlemopu  7701  caucvgprprlemupu  7702  caucvgprprlemdisj  7704  caucvgprprlemloc  7705  caucvgprprlemexbt  7708  caucvgprprlemaddq  7710  caucvgprprlemlim  7713  suplocexprlemss  7717  suplocexprlemrl  7719  suplocexprlemmu  7720  suplocexprlemru  7721  suplocexprlemdisj  7722  suplocexprlemloc  7723  suplocexprlemub  7725  suplocexprlemlub  7726  recexgt0sr  7775  mulgt0sr  7780  archsr  7784  caucvgsrlemoffcau  7800  suplocsrlemb  7808  suplocsrlempr  7809  suplocsrlem  7810  cnm  7834  axarch  7893  axcaucvglemcau  7900  axpre-suploclemres  7903  lelttr  8049  ltletr  8050  ltled  8079  cnegexlem1  8135  cnegexlem2  8136  renegcl  8221  negf1o  8342  gt0add  8533  apreap  8547  apirr  8565  apsym  8566  apcotr  8567  apadd1  8568  apneg  8571  mulext1  8572  mulap0r  8575  apti  8582  aprcl  8606  aptap  8610  recexap  8613  mulap0  8614  receuap  8629  mul0eqap  8630  lep1  8805  lem1  8807  letrp1  8808  recreclt  8860  lbinf  8908  suprubex  8911  nnrecgt0  8960  bndndx  9178  nn0ge2m1nn  9239  elnn0z  9269  peano2z  9292  zaddcl  9296  ztri3or0  9298  zltnle  9302  zdceq  9331  zdcle  9332  zdclt  9333  zdiv  9344  zeo  9361  fnn0ind  9372  btwnz  9375  uzm1  9561  uzp1  9564  indstr  9596  supinfneg  9598  infsupneg  9599  eluzdc  9613  nn01to3  9620  qapne  9642  xrltled  9802  xrlelttr  9809  xrltletr  9810  ge0nemnf  9827  fzdcel  10043  elfzouz2  10164  fzoss1  10174  fzospliti  10179  fzocatel  10202  fzostep1  10240  qtri3or  10246  qltnle  10249  qdceq  10250  exbtwnzlemex  10253  rebtwn2zlemstep  10256  rebtwn2z  10258  qbtwnxr  10261  ioom  10264  ico0  10265  ioc0  10266  flqeqceilz  10321  modqadd1  10364  modqmul1  10380  frec2uzuzd  10405  frec2uzlt2d  10407  frec2uzf1od  10409  frecuzrdgrrn  10411  frec2uzrdg  10412  frecuzrdgrcl  10413  frecuzrdgsuc  10417  frecuzrdgrclt  10418  frecuzrdgdomlem  10420  uzsinds  10445  seqvalcd  10462  seqovcd  10466  seq3fveq2  10472  seq3shft2  10476  monoord  10479  seq3split  10482  seq3caopr3  10484  iseqf1olemab  10492  iseqf1olemnanb  10493  iseqf1olemqk  10497  seq3id3  10510  seq3id2  10512  seq3homo  10513  expgt1  10561  m1expeven  10570  expnbnd  10647  expnlbnd2  10649  nn0ltexp2  10692  apexp1  10701  hashennn  10763  zfz1isolem1  10823  seq3coll  10825  cjap  10918  caucvgre  10993  cvg1nlemres  10997  resqrexlemgt0  11032  resqrexlemglsq  11034  resqrexlemga  11035  resqrtcl  11041  abslt  11100  abssubap0  11102  abssubne0  11103  caubnd2  11129  qdenre  11214  maxabslemlub  11219  maxabs  11221  maxleast  11225  fimaxre2  11238  xrmaxiflemlub  11259  xrmaxif  11262  xrmaxltsup  11269  xrmaxadd  11272  xrmineqinf  11280  climuni  11304  2clim  11312  climcn1  11319  climcn2  11320  subcn2  11322  mulcn2  11323  climsqz  11346  climsqz2  11347  climcau  11358  climcvg1nlem  11360  climcaucn  11362  serf0  11363  sumrbdclem  11388  summodclem2  11393  zsumdc  11395  divcnv  11508  absltap  11520  absgtap  11521  mertenslem2  11547  ntrivcvgap  11559  prodrbdclem  11582  prodmodclem2  11588  zproddc  11590  prodssdc  11600  fprodsplitdc  11607  fprodcl2lem  11616  efcllemp  11669  tanvalap  11719  sin01bnd  11768  cos01bnd  11769  sin01gt0  11772  absef  11780  eirrap  11788  dvds0  11816  dvdsmul1  11823  dvdsmultr1d  11842  dvdslelemd  11852  divconjdvds  11858  alzdvds  11863  sqoddm1div8z  11894  nno  11914  divalglemex  11930  zsupcllemstep  11949  zsupcl  11951  infssuzledc  11954  dvdsbnd  11960  dvdslegcd  11968  zeqzmulgcd  11974  gcd0id  11983  gcdaddm  11988  gcd1  11991  gcdabs  11992  bezoutlemnewy  12000  bezoutlemstep  12001  bezoutlemmain  12002  bezoutlemex  12005  bezoutlemzz  12006  bezoutlemaz  12007  bezoutlembz  12008  bezoutlembi  12009  bezoutlemle  12012  bezoutlemsup  12013  mulgcd  12020  gcdzeq  12026  dvdsmulgcd  12029  sqgcd  12033  bezoutr1  12037  algcvga  12054  algfx  12055  eucalglt  12060  eucalg  12062  lcmneg  12077  lcmabs  12079  lcmgcdlem  12080  ncoprmgcdne1b  12092  mulgcddvds  12097  qredeq  12099  divgcdcoprm0  12104  cncongr1  12106  isprm2lem  12119  nprm  12126  dvdsnprmd  12128  prmdvdsfz  12142  isprm5lem  12144  coprm  12147  isprm6  12150  sqrt2irr  12165  pw2dvdslemn  12168  pw2dvdseulemle  12170  oddpwdclemdvds  12173  oddpwdclemndvds  12174  sqrt2irrap  12183  qnumdencl  12190  prmdiv  12238  modprmn0modprm0  12259  prm23lt5  12266  pythagtriplem4  12271  pythagtriplem19  12285  pythagtrip  12286  pclemub  12290  pcpre1  12295  pcpremul  12296  pceulem  12297  pcqcl  12309  pcidlem  12325  pcgcd1  12330  pc2dvds  12332  dvdsprmpweqle  12339  difsqpwdvds  12340  pcadd  12342  pcmpt  12344  expnprm  12354  pockthg  12358  infpnlem2  12361  prmunb  12363  1arith  12368  4sqlem10  12388  ennnfonelemex  12418  ennnfonelemhom  12419  ennnfonelemrnh  12420  ennnfonelemnn0  12426  ennnfonelemim  12428  exmidunben  12430  ctinfomlemom  12431  ctinfom  12432  ctinf  12434  omctfn  12447  nninfdclemp1  12454  setscomd  12506  imasaddfnlemg  12741  mhmf1o  12868  grpinveu  12918  grpasscan1  12940  dfgrp3mlem  12975  grp1inv  12984  issubg4m  13063  srgisid  13180  ringadd2  13221  ringinvnzdiv  13238  unitgrp  13296  ringelnzr  13339  lringuplu  13348  subrguss  13368  subrgintm  13375  aprcotr  13386  islmodd  13394  lssclg  13462  lss0cl  13467  lssvneln0  13471  lss1d  13481  lmodindp1  13526  tgcl  13725  neii1  13808  neii2  13810  neiss  13811  tpnei  13821  tgrest  13830  ssrest  13843  icnpimaex  13872  lmcvg  13878  cnpnei  13880  cnptopco  13883  lmff  13910  txcnp  13932  txcn  13936  hmeontr  13974  blssec  14099  mopni3  14145  blsscls2  14154  comet  14160  bdxmet  14162  bdmopn  14165  xmettxlem  14170  xmettx  14171  addcncntoplem  14212  mulc1cncf  14237  cncfco  14239  cncfmptc  14243  mulcncflem  14251  mulcncf  14252  dedekindeulemlu  14260  dedekindeulemeu  14261  suplociccreex  14263  suplociccex  14264  dedekindicclemlu  14269  dedekindicclemeu  14270  ivthinclemlopn  14275  ivthinclemlr  14276  ivthinclemuopn  14277  ivthinclemur  14278  ivthinclemloc  14280  ivthinc  14282  limcimolemlt  14294  limcresi  14296  cnplimcim  14297  cnplimclemle  14298  cnplimclemr  14299  limccnpcntop  14305  limccoap  14308  dvcoapbr  14332  dvcj  14334  efltlemlt  14356  sin0pilem2  14364  tangtx  14420  logdivlti  14463  rplogbval  14524  logbgcd1irraplemexp  14547  logbgcd1irraplemap  14548  logbgcd1irrap  14549  lgsval4a  14584  lgsdir2lem3  14592  lgsne0  14600  lgseisenlem1  14611  2lgsoddprmlem2  14615  2sqlem8a  14630  2sqlem8  14631  2sqlem9  14632  bj-exlimmpi  14683  uzdcinzz  14711  bj-charfundcALT  14722  bj-2inf  14851  bj-peano4  14868  bj-nn0suc  14877  1dom1el  14904  subctctexmid  14912  nninfalllem1  14919  nninfsellemqall  14926  nninfomnilem  14929  nninffeq  14931  exmidsbthrlem  14932  sbthomlem  14935  refeq  14938  isomninnlem  14940  apdifflemr  14957  redcwlpo  14965  reap0  14968  nconstwlpolem  14975