Theorem mpd 13

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

Hypotheses

Ref	Expression
mpd.1	|- ( ph -> ps )
mpd.2	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
mpd	|- ( ph -> ch )

Proof of Theorem mpd

Step	Hyp	Ref	Expression
1		mpd.1	. 2 |- ( ph -> ps )
2		mpd.2	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	a2i 11	. 2 |- ( ( ph -> ps ) -> ( ph -> ch ) )
4	1, 3	ax-mp 5	1 |- ( ph -> ch )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-2 7

This theorem is used 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  3828  preq12b  3895  axpweq  4308  exmid1dc  4337  exmid1stab  4345  opth  4377  issod  4464  frirrg  4495  frind  4497  ralxfr2d  4610  rexxfr2d  4611  eldifpw  4623  onun2  4637  onuni  4641  elirr  4688  en2lp  4701  wetriext  4724  peano2  4742  relop  4930  elres  5099  sotri2  5185  iota4an  5358  iota5  5359  funeu  5402  funopg  5411  imadiflem  5460  funimaexglem  5464  ssimaex  5764  ffvelcdm  5841  dff3im  5853  dffo4  5856  funopsn  5891  f1eqcocnv  5997  f1oiso2  6033  riota5f  6065  riotass2  6067  acexmidlemcase  6080  elovimad  6129  ovmpodf  6220  ovmpodv2  6222  ovi3  6226  ov6g  6227  caoftrn  6335  op1steq  6413  fvdifsuppst  6484  suppssdc  6500  suppofss1dcl  6504  suppofss2dcl  6505  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemi14d  6604  tfr1onlembxssdm  6614  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllembxssdm  6627  tfrcllemaccex  6632  tfrcllemres  6633  rdgivallem  6652  nnsucelsuc  6764  nnsucsssuc  6765  dcdifsnid  6777  nnawordex  6802  ersym  6819  mapvalg  6932  pmvalg  6933  mapsnd  6970  mapsn  6972  fundmen  7094  1dom1el  7107  en2  7112  pw2f1odclem  7134  mapdom1g  7147  fidceq  7171  fin0or  7190  findcard2  7193  findcard2s  7194  fidcen  7203  prfidceq  7235  fiintim  7238  suplub2ti  7341  supsnti  7345  supisoex  7349  difinfsnlem  7439  difinfsn  7440  ctm  7449  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  enumctlemm  7454  nninfninc  7463  nnnninfeq2  7469  enomnilem  7478  exmidomniim  7481  exmidomni  7482  fodjuomnilemdc  7484  fodjuomnilemres  7488  omnimkv  7496  mkvprop  7498  omniwomnimkv  7507  en2prde  7539  pr2cv1  7541  en2eleq  7547  acfun  7563  exmidontriimlem1  7577  exmidontriimlem4  7580  exmidontriim  7581  papsym  7612  papcotr  7613  ccfunen  7630  cc4f  7635  cc4n  7637  elni2  7681  mulclpi  7695  nlt1pig  7708  indpi  7709  recclnq  7759  ltexnqq  7775  halfnqq  7777  prarloclemarch  7785  prarloclemarch2  7786  prop  7842  prltlu  7854  prarloclem3step  7863  prarloclem5  7867  prarloclem  7868  prarloc  7870  prarloc2  7871  genpml  7884  genpmu  7885  genprndl  7888  genprndu  7889  genpdisj  7890  addnqprllem  7894  addnqprulem  7895  addlocprlemeq  7900  addlocprlemgt  7901  addlocprlem  7902  addlocpr  7903  nqprloc  7912  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  appdivnq  7930  prmuloc  7933  prmuloc2  7934  mullocprlem  7937  mullocpr  7938  mulnqprlemrl  7940  mulnqprlemru  7941  ltprordil  7956  ltpopr  7962  ltsopr  7963  ltaddpr  7964  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  ltaprg  7986  recexprlemm  7991  recexprlem1ssl  8000  recexprlem1ssu  8001  aptiprleml  8006  aptiprlemu  8007  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlem1  8026  archrecpr  8031  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlem1  8046  caucvgprlemlim  8048  caucvgprprlemnbj  8060  caucvgprprlemml  8061  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemupu  8067  caucvgprprlemdisj  8069  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  caucvgprprlemlim  8078  suplocexprlemss  8082  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  recexgt0sr  8140  mulgt0sr  8145  archsr  8149  caucvgsrlemoffcau  8165  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  cnm  8199  axarch  8258  axcaucvglemcau  8265  axpre-suploclemres  8268  lelttr  8414  ltletr  8415  ltled  8445  cnegexlem1  8501  cnegexlem2  8502  renegcl  8587  negf1o  8709  gt0add  8901  apreap  8915  apirr  8933  apsym  8934  apcotr  8935  apadd1  8936  apneg  8939  mulext1  8940  mulap0r  8943  apti  8950  aprcl  8974  aptap  8978  recexap  8981  mulap0  8982  receuap  8999  mul0eqap  9000  lep1  9175  lem1  9177  letrp1  9178  recreclt  9230  lbinf  9278  suprubex  9281  nnrecgt0  9342  bndndx  9562  nn0ge2m1nn  9627  elnn0z  9657  peano2z  9680  zaddcl  9684  ztri3or0  9686  zltnle  9690  zdceq  9720  zdcle  9721  zdclt  9722  zdiv  9734  zeo  9751  fnn0ind  9762  btwnz  9765  uzm1  9953  uzp1  9956  indstr  9993  supinfneg  9995  infsupneg  9996  eluzdc  10010  nn01to3  10017  qapne  10039  xrltled  10201  xrlelttr  10208  xrltletr  10209  ge0nemnf  10226  fzdcel  10444  elfzouz2  10569  fzoss1  10580  fzospliti  10585  elincfzoext  10611  fzocatel  10617  fzostep1  10656  zsupcllemstep  10662  zsupcl  10664  infssuzledc  10667  qtri3or  10675  qltnle  10678  qdceq  10679  qdclt  10680  exbtwnzlemex  10684  rebtwn2zlemstep  10687  rebtwn2z  10689  qbtwnxr  10692  ioom  10695  ico0  10696  ioc0  10697  flqeqceilz  10755  modqadd1  10798  modqmul1  10814  frec2uzuzd  10839  frec2uzlt2d  10841  frec2uzf1od  10843  frecuzrdgrrn  10845  frec2uzrdg  10846  frecuzrdgrcl  10847  frecuzrdgsuc  10851  frecuzrdgrclt  10852  frecuzrdgdomlem  10854  uzsinds  10881  seqvalcd  10898  seqovcd  10904  seq3fveq2  10912  seqfveq2g  10914  seq3shft2  10918  seqshft2g  10919  monoord  10922  seq3split  10925  seqsplitg  10926  seq3caopr3  10928  iseqf1olemab  10939  iseqf1olemnanb  10940  iseqf1olemqk  10944  seqf1oglem1  10956  seqf1og  10958  seq3id3  10961  seq3id2  10963  seq3homo  10964  seqhomog  10967  expgt1  11014  m1expeven  11023  expnbnd  11101  expnlbnd2  11103  nn0ltexp2  11147  apexp1  11156  hashennn  11219  hashfibclem  11282  hashf1lem2  11286  zfz1isolem1  11292  seq3coll  11294  pfxwrdsymbg  11462  wrdind  11494  wrd2ind  11495  cjap  11672  caucvgre  11747  cvg1nlemres  11751  resqrexlemgt0  11786  resqrexlemglsq  11788  resqrexlemga  11789  resqrtcl  11795  abslt  11854  abssubap0  11856  abssubne0  11857  caubnd2  11883  qdenre  11968  maxabslemlub  11973  maxabs  11975  maxleast  11979  fimaxre2  11993  xrmaxiflemlub  12014  xrmaxif  12017  xrmaxltsup  12024  xrmaxadd  12027  xrmineqinf  12035  climuni  12059  2clim  12067  climcn1  12074  climcn2  12075  subcn2  12077  mulcn2  12078  climsqz  12101  climsqz2  12102  climcau  12113  climcvg1nlem  12115  climcaucn  12117  serf0  12118  sumrbdclem  12144  summodclem2  12149  zsumdc  12151  divcnv  12264  absltap  12276  absgtap  12277  mertenslem2  12303  ntrivcvgap  12315  prodrbdclem  12338  prodmodclem2  12344  zproddc  12346  prodssdc  12356  fprodsplitdc  12363  fprodcl2lem  12372  efcllemp  12425  tanvalap  12475  sin01bnd  12524  cos01bnd  12525  sin01gt0  12529  absef  12537  eirrap  12545  dvds0  12573  dvdsmul1  12580  dvdsmultr1d  12599  dvdslelemd  12610  divconjdvds  12616  alzdvds  12621  3dvds  12631  sqoddm1div8z  12653  nno  12673  divalglemex  12689  bits0o  12717  dvdsbnd  12733  dvdslegcd  12741  zeqzmulgcd  12747  gcd0id  12756  gcdaddm  12761  gcd1  12764  gcdabs  12765  bezoutlemnewy  12773  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlemex  12778  bezoutlemzz  12779  bezoutlemaz  12780  bezoutlembz  12781  bezoutlembi  12782  bezoutlemle  12785  bezoutlemsup  12786  mulgcd  12793  gcdzeq  12799  dvdsmulgcd  12802  sqgcd  12806  bezoutr1  12810  nninfctlemfo  12817  algcvga  12829  algfx  12830  eucalglt  12835  eucalg  12837  lcmneg  12852  lcmabs  12854  lcmgcdlem  12855  ncoprmgcdne1b  12867  mulgcddvds  12872  qredeq  12874  divgcdcoprm0  12879  cncongr1  12881  isprm2lem  12894  nprm  12901  dvdsnprmd  12903  prmdvdsfz  12917  isprm5lem  12919  coprm  12922  isprm6  12925  sqrt2irr  12940  pw2dvdslemn  12943  pw2dvdseulemle  12945  oddpwdclemdvds  12948  oddpwdclemndvds  12949  sqrt2irrap  12958  qnumdencl  12965  prmdiv  13013  modprmn0modprm0  13035  prm23lt5  13042  pythagtriplem4  13047  pythagtriplem19  13061  pythagtrip  13062  pclemub  13066  pcpre1  13071  pcpremul  13072  pceulem  13073  pcqcl  13085  pcidlem  13102  pcgcd1  13107  pc2dvds  13109  dvdsprmpweqle  13116  difsqpwdvds  13117  pcadd  13119  pcmpt  13122  expnprm  13132  pockthg  13136  infpnlem2  13139  prmunb  13141  1arith  13146  4sqlem10  13166  4sqlem11  13180  4sqlem12  13181  4sqlem13m  13182  4sqlem17  13186  4sqlem18  13187  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemfrceq  13272  ennnfonelemex  13305  ennnfonelemhom  13306  ennnfonelemrnh  13307  ennnfonelemnn0  13313  ennnfonelemim  13315  exmidunben  13317  ctinfomlemom  13318  ctinfom  13319  ctinf  13321  omctfn  13334  nninfdclemp1  13341  setscomd  13393  imasaddfnlemg  13635  mhmf1o  13777  grpinveu  13843  grpasscan1  13868  dfgrp3mlem  13903  grp1inv  13912  issubg4m  13996  ghmf1o  14078  srgisid  14290  ringadd2  14332  ringinvnzdiv  14355  unitgrp  14423  ringelnzr  14494  lringuplu  14503  subrguss  14544  subrgintm  14551  aprcotr  14597  islmodd  14629  lssclg  14701  lss0cl  14706  lssvneln0  14710  lss1d  14720  lmodindp1  14765  rnglidlmmgm  14833  znidomb  14993  znunit  14994  znrrg  14995  rnasclassa  15038  mplsubgfilemcl  15090  mplsubgfileminv  15091  tgcl  15165  neii1  15248  neii2  15250  neiss  15251  tpnei  15261  tgrest  15270  ssrest  15283  icnpimaex  15312  lmcvg  15318  cnpnei  15320  cnptopco  15323  lmff  15350  txcnp  15372  txcn  15376  hmeontr  15414  blssec  15539  mopni3  15585  blsscls2  15594  comet  15600  bdxmet  15602  bdmopn  15605  xmettxlem  15610  xmettx  15611  addcncntoplem  15662  mpomulcn  15667  mulc1cncf  15690  cncfco  15692  cncfmptc  15697  mulcncflem  15708  mulcncf  15709  dedekindeulemlu  15722  dedekindeulemeu  15723  suplociccreex  15725  suplociccex  15726  dedekindicclemlu  15731  dedekindicclemeu  15732  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemloc  15742  ivthinc  15744  ivthreinc  15746  ivthdichlem  15752  limcimolemlt  15765  limcresi  15767  cnplimcim  15768  cnplimclemle  15769  cnplimclemr  15770  limccnpcntop  15776  limccoap  15779  dvcoapbr  15808  dvcj  15810  plyf  15838  plyaddlem1  15848  plymullem1  15849  plyco  15860  plycj  15862  plycn  15863  plyrecj  15864  dvply2g  15867  efltlemlt  15875  sin0pilem2  15883  tangtx  15939  logdivlti  15982  rplogbval  16047  logbgcd1irraplemexp  16070  logbgcd1irraplemap  16071  logbgcd1irrap  16072  birthdaylem1g  16087  perfect1  16112  perfectlem1  16113  perfectlem2  16114  lgsval4a  16141  lgsdir2lem3  16149  lgsne0  16157  gausslemma2dlem3  16182  gausslemma2dlem4  16183  gausslemma2dlem6  16186  gausslemma2dlem7  16187  gausslemma2d  16188  lgseisenlem1  16189  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem2  16201  lgsquad3  16203  2lgsoddprmlem2  16225  2sqlem8a  16241  2sqlem8  16242  2sqlem9  16243  lpvtx  16320  upgrex  16344  upgr1een  16365  edgupgren  16382  umgredg  16386  upgrpredgv  16387  upgredg2vtx  16389  upgredgpr  16390  uspgrf1oedg  16417  usgredg4  16456  uspgredgdomord  16470  usgr1vr  16489  wlkvtxiedg  16586  wlkvtxiedgg  16587  wlk1walkdom  16600  upgriswlkdc  16601  upgrwlkedg  16602  uspgr2wlkeq  16606  uspgr2wlkeqi  16608  umgrwlknloop  16609  eupth2lem2dc  16700  trlsegvdeglem1  16701  eupth2lem3lem4fi  16714  bj-exlimmpi  16798  uzdcinzz  16826  bj-charfundcALT  16835  bj-2inf  16964  bj-peano4  16981  bj-nn0suc  16990  pw1ndom3  17020  subctctexmid  17030  exmidcon  17037  nninfalllem1  17051  nninfsellemqall  17058  nninfomnilem  17061  nninffeq  17063  nnnninfex  17065  exmidsbthrlem  17067  sbthomlem  17070  refeq  17073  isomninnlem  17079  apdifflemr  17096  redcwlpo  17105  reap0  17108  nconstwlpolem  17115