Theorem mpdan 699

Description: An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

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

Assertion

Ref	Expression
mpdan	⊢ (𝜑 → 𝜒)

Proof of Theorem mpdan

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜑 → 𝜑)
2		mpdan.1	. 2 ⊢ (𝜑 → 𝜓)
3		mpdan.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  mpidan  701  mpan2  703  biadanid  834  mpjaodan  973  mpjao3dan  1457  mpd3an3  1489  elabd2  3628  eueq2  3672  csbiegf  3885  difsnb  4773  reusv3i  5375  frpoinsg  6344  fimadmfo  6801  fimadmfoALT  6803  fvtresfn  6992  fvmpt3  6994  ffvelcdmd  7080  fnressn  7155  fsnex  7281  f1oiso2  7350  riota5f  7395  onsuc  7808  onsucuni  7823  frrlem10  8291  seqomlem2  8437  oaordi  8530  nnaordi  8603  qsdisj  8791  dom2lem  8988  canth2g  9118  limenpsi  9139  nnfi  9151  php4  9193  onfin  9198  sucxpdom  9220  dmfi  9291  fiin  9381  supiso  9435  ordiso2  9476  wdom2d  9541  elirrvOLD  9559  infeq5  9605  cantnfp1lem3  9648  cantnflem1d  9656  rankwflemb  9764  onenon  9934  cardonle  9942  sdomsdomcardi  9956  acni  10028  cardaleph  10072  djuen  10152  djuinf  10171  infdju1  10172  nnadju  10180  pwsdompw  10185  infdif  10190  cfval  10229  fin34  10373  fin1a2lem1  10383  fin1a2  10398  ttukeylem6  10497  sdomsdomcard  10543  canth3  10544  fpwwe2  10627  canthwelem  10634  gchdju1  10640  pwfseqlem4  10646  gchdjuidm  10652  gchxpidm  10653  tskwe2  10757  rankcf  10761  tskuni  10767  gruxp  10791  dmrecnq  10952  lterpq  10954  archnq  10964  reclem3pr  11033  reclem4pr  11034  0idsr  11081  lep1  12055  ledivp1  12116  negfi  12163  supaddc  12181  supmul1  12183  suprzcl  12675  uz11  12886  zmin  12967  zbtwnre  12969  rpnnen1lem4  13003  rpnnen1lem5  13004  xnegid  13263  supxrre  13352  infxrre  13362  eluzfz2  13559  fzsuc  13598  fzsuc2  13609  fzp1disj  13610  fzneuz  13635  nn0p1elfzo  13730  fllep1  13833  fraclt1  13834  fracle1  13835  fracge0  13836  flhalf  13862  ceige  13876  ceim1l  13879  fldiv  13892  modval  13903  suppssfz  14029  seqeq1  14039  expubnd  14213  iexpcyc  14242  binom2sub1  14256  faclbnd4lem3  14330  pfxid  14721  pfxccatpfx2  14773  swrdccat3blem  14775  cshw0  14830  cshwn  14833  cshimadifsn  14865  cshimadifsn0  14866  pfx2  14983  trclexlem  15030  shftfval  15106  shftcan1  15119  sgnneg  15136  reval  15156  cjmulrcl  15194  addcj  15198  absval  15288  absneg  15327  abscj  15329  sqabsadd  15332  sqabssub  15333  leabs  15349  sqreulem  15410  lo1res  15609  o1of2  15663  o1rlimmul  15669  fsumconst1  15841  flo1  15907  trirecip  15916  efcan  16149  efi4p  16192  resin4p  16193  recos4p  16194  sincossq  16231  ruclem10  16294  iddvds  16326  1dvds  16327  2ebits  16504  lcmftp  16693  coprmgcdb  16706  1idssfct  16737  exprmfct  16762  eulerthlem2  16840  odzphi  16855  pcprendvds  16899  pcmpt  16951  oddprmdvds  16962  vdwlem8  17047  0ram2  17080  prmgaplem7  17116  setsn0fun  17232  setsexstruct2  17234  pwsvscaval  17548  2initoinv  18066  initoeu1  18067  initoeu2lem1  18070  initoeu2  18072  2termoinv  18073  termoeu1  18074  homarel  18092  joinfval  18426  meetfval  18440  latjcom  18502  latmcom  18518  0subm  18875  sgrp2nmndlem5  18990  grprcan  19039  isgrpid2  19042  grpinvid  19065  mulgnn0z  19166  qus0  19259  eqg0subg  19266  ghmker  19311  symgbasmap  19446  symginv  19471  pmtrfrn  19527  odmulg2  19624  slwpgp  19682  pj1eq  19769  efgtf  19791  frgpinv  19833  frgpup2  19845  cnaddablx  19937  cnaddabl  19938  zaddablx  19941  imasabl  19945  dprdfadd  20091  dpjidcl  20129  dpjlid  20132  pgpfac1lem3  20148  omndmul2  20202  omndmul  20204  rngen1zr0  20261  srgen1zr0  20297  1unit  20455  unitgrpid  20466  1rinv  20476  irredn0  20504  irredneg  20511  c0snmgmhm  20543  rngisomring1  20549  zrrnghm  20620  rnrhmsubrg  20689  zrinitorngc  20726  zrtermorngc  20727  zrtermoringc  20759  isdrng2  20828  abv0  20905  abv1z  20906  abvneg  20908  orng0le1  20956  lmodfopne  21000  lsssn0  21048  lspsn0  21108  lsp0  21109  lmhmvsca  21145  lmhmrnlss  21150  lmhmkerlss  21151  lsppratlem5  21254  rsp1  21345  kerlidl  21396  ring2idlqus  21428  rngqiprngfulem4  21433  rngqiprngfu  21436  ssdifidllem  21463  cnfldneg  21527  zringcyg  21598  chrid  21654  chrrhm  21660  ip0r  21766  ocvlss  21801  ocv1  21808  rlmassa  21999  psrbagfsupp  22048  snifpsrbag  22049  psrbaglefi  22055  psrvscaval  22079  psrdi  22093  psrdir  22094  mplvscaval  22144  mhpmpl  22286  mhpdeg  22287  mhppwdeg  22292  psdmul  22308  psdpw  22312  coe1sclmulfv  22423  coe1id  22433  evl1var  22475  mamuvs1  22541  mamuvs2  22542  matecl  22561  matvscacell  22572  mat0scmat  22674  submaval0  22716  mdetrsca  22739  maduval  22774  minmar1val0  22783  pmatcollpw3fi1lem2  22923  chcoeffeqlem  23021  cayleyhamilton0  23025  cayleyhamiltonALT  23027  toponsspwpw  23058  cctop  23142  cldval  23159  ntrfval  23160  clsfval  23161  cmclsopn  23198  opncldf3  23222  neifval  23235  lpfval  23274  cnrmnrm  23497  dis2ndc  23596  islocfin  23653  tx1cn  23745  idqtop  23842  kqtopon  23863  kqid  23864  kqcld  23871  hmphen2  23935  filssufil  24048  ufileu  24055  alexsublem  24180  efmndtmd  24237  symgtgp  24242  ustuqtop4  24380  cstucnd  24419  metustexhalf  24692  nm0  24765  rlmnlm  24824  nmolb  24853  metdseq0  24991  pi1xfrval  25192  clmvneg1  25237  clmvsubval  25247  ipcau2  25372  tcphcphlem1  25373  tcphcphlem2  25374  cmetcaulem  25426  ovolicc2lem3  25657  ovolicc2lem4  25658  mbfmulc2lem  25785  i1fpos  25844  mbfi1fseqlem3  25855  itg2ge0  25873  bddiblnc  25980  dvres2  26050  dvaddbr  26076  dvmulbr  26077  dvcobr  26084  dvfsumlem4  26167  ftc1a  26175  ftc1lem6  26179  uc1pmon1p  26288  ig1pval2  26313  dgradd2  26404  dgrcolem2  26410  plydivlem4  26436  plydiveu  26438  elqaalem3  26461  qaa  26463  ulmdvlem1  26539  abelthlem6  26575  abelthlem7  26577  eflogeq  26743  jensenlem2  27128  harmonicbnd4  27151  sgmnncl  27287  dchrptlem2  27405  1lgs  27480  lgs1  27481  2sqcoprm  27575  addsqnreup  27583  dchrisumlem2  27630  dchrisum0lem2a  27657  selberg2lem  27690  pntrsumo1  27705  pntrsumbnd  27706  pntpbnd1  27726  pntlemr  27742  pntlemj  27743  padicabvf  27771  bdayval  27788  noextendgt  27810  nosupbnd2lem1  27855  noinfbnd2lem1  27870  noetainflem4  27880  oldval  28003  divmuls  28390  divscl  28392  seqsp1  28480  bdayfinbndlem1  28636  zz12s  28644  remulscllem1  28669  plngrotlem2  29044  incistruhgr  29395  subgrprop3  29592  subgruhgredgd  29600  usgrexi  29757  cusgrexi  29759  cusgrsizeinds  29768  vtxdgfusgrf  29813  1hevtxdg1  29822  1egrvtxdg1  29825  ewlkprop  29919  wlklenvm1  29937  wlkl1loop  29953  wlkp1lem4  29990  2pthnloop  30046  upgrclwlkcompim  30096  crctcshwlkn0lem4  30128  crctcshwlkn0lem5  30129  crctcshwlkn0lem6  30130  crctcshwlkn0lem7  30131  crctcshlem4  30135  wspthnonp  30174  wlkswwlksf1o  30194  wwlksnwwlksnon  30230  umgr2wlkon  30265  wwlks2onv  30268  elwwlks2ons3im  30269  elwspths2spth  30285  umgrclwwlkge2  30308  clwlkclwwlkf1lem3  30323  erclwwlkref  30337  clwwlknp  30354  wwlksext2clwwlk  30374  wwlksubclwwlk  30375  0pthon1  30445  1wlkdlem4  30457  1pthd  30460  3spthd  30493  eupth2eucrct  30534  eucrctshift  30560  eucrct2eupth  30562  frgrncvvdeqlem8  30623  frgr2wwlkeqm  30648  isgrpoi  30816  grpoinvfval  30840  grpodivfval  30852  vcz  30893  cnaddabloOLD  30899  nvz0  30986  sspz  31053  lno0  31074  nmobndi  31093  ipasslem2  31150  shunssi  31686  ococin  31726  ssjo  31765  pjocini  32016  nlfnval  32199  lncnopbd  32355  riesz3i  32380  cnlnadjlem7  32391  pjclem4  32517  pj3si  32525  hstoc  32540  hstnmoc  32541  hstoh  32550  hst0  32551  mdsl2i  32640  chirredlem3  32710  chirredlem4  32711  dmdbr5ati  32740  rexunirn  32804  fcnvgreu  32983  infxrge0glb  33076  cycpmco2lem5  33416  cycpmco2lem6  33417  cycpmco2lem7  33418  isarchi3  33473  rlocisunit  33562  nsgqusf1olem2  33689  ssmxidllem  33722  rprmdvdspow  33789  ressply1sub  33826  selvply1rhmlemb  33875  fedgmullem1  33985  extdg1id  34022  nn0constr  34117  zartopn  34231  zarcmplem  34237  esumcvg  34442  esumcvgre  34447  sigaval  34467  unelldsys  34514  fiunelros  34530  measval  34554  pmeasmono  34680  probfinmeasb  34784  ballotlemfc0  34849  ballotlemfcc  34850  ballotlemsi  34871  ballotlemfrci  34884  signlem0  34940  breprexp  34986  bnj1006  35314  bnj1110  35336  bnj1253  35371  bnj1280  35374  bnj1463  35409  bnj1312  35412  fineqvinfep  35492  erdszelem7  35643  erdszelem8  35644  cvmliftlem10  35740  cvmliftlem13  35742  cvmlift2lem9  35757  cvmlift3lem6  35770  cvmlift3lem7  35771  cvmlift3lem9  35773  satfv1lem  35808  dfrdg2  36239  cldregopn  36786  tailfval  36827  filnetlem3  36835  filnetlem4  36836  ontopbas  36883  bj-nnfbd  37338  bj-elid4  37756  bj-imdiridlem  37773  f1omptsnlem  37926  icoreunrn  37949  relowlpssretop  37954  fvineqsnf1  38000  wl-sbal2  38163  unccur  38198  poimirlem1  38216  poimirlem2  38217  poimirlem4  38219  poimirlem6  38221  poimirlem7  38222  poimirlem11  38226  poimirlem12  38227  poimirlem17  38232  poimirlem20  38235  poimirlem22  38237  poimirlem23  38238  poimirlem28  38243  poimir  38248  ismblfin  38256  cnambfre  38263  ftc1cnnc  38287  dvasin  38299  ismtyres  38403  heiborlem8  38413  ghomidOLD  38484  rngosn6  38521  rngonegmn1l  38536  rngonegmn1r  38537  rngoneglmul  38538  rngonegrmul  38539  idlnegcl  38617  0idl  38620  0rngo  38622  smprngopr  38647  sucmapsuc  39084  cossex  39104  qsdisjALTV  39294  cnvepresdmqss  39332  mpets2  39550  lkrval  39808  ldualvaddval  39851  ldualvsval  39858  opoc1  39922  pmap0  40485  pmap1N  40487  pexmidALTN  40698  cdleme31fv  41110  cdlemg27b  41416  erngdvlem4  41711  erng0g  41714  erngdvlem4-rN  41719  dvalveclem  41745  dvh0g  41831  dih0cnv  42003  dih1rn  42007  dih1cnv  42008  doch0  42078  doch1  42079  lcfl7lem  42219  mapdheq  42448  hdmap1eq  42521  hdmapval2lem  42551  hgmapvvlem3  42645  zndvdchrrhm  42686  lcmineqlem13  42754  aks4d1p9  42801  primrootsunit1  42810  aks6d1c1p1  42820  aks6d1c1p6  42827  aks6d1c1p8  42828  sticksstones1  42859  sticksstones6  42864  sticksstones7  42865  sticksstones11  42869  sticksstones12a  42870  sticksstones12  42871  sticksstones22  42881  aks6d1c6isolem1  42887  aks6d1c6isolem2  42888  unitscyglem5  42912  renegid  43080  sn-0ne2  43113  remul01  43114  remulinvcom  43140  sn-0tie0  43171  renegmulnnass  43185  domnexpgn0cl  43239  abvexp  43248  frlmsnic  43256  fsuppssind  43273  mzpval  43411  mzpindd  43425  pellex  43510  2nn0ind  43620  jm2.26lem3  43676  pw2f1o2val  43714  wepwsolem  43717  fnwe2lem3  43727  lnmfg  43757  dgrsub2  43810  mpaaeu  43825  flcidc  43845  dflim5  44004  naddwordnexlem1  44072  rtrclexlem  44290  cnvrcl0  44299  brcoffn  44704  clsk1indlem3  44717  clsneif1o  44778  clsneicnv  44779  clsneikex  44780  clsneinex  44781  neicvgmex  44791  neicvgel1  44793  suprleubrd  44840  suprlubrd  44842  imo72b2  44846  dvconstbi  44992  bcc0  44998  binomcxplemnotnn0  45014  nnfoctb  45716  infleinflem1  46033  fprodcnlem  46263  sumnnodd  46294  icccncfext  46549  itgsin0pilem1  46612  stoweidlem32  46694  stoweidlem35  46697  stoweidlem36  46698  stoweidlem37  46699  stoweidlem43  46705  stoweidlem50  46712  wallispilem5  46731  stirlinglem2  46737  stirlinglem3  46738  stirlinglem4  46739  stirlinglem8  46743  stirlinglem11  46746  stirlinglem12  46747  stirlinglem14  46749  stirlinglem15  46750  fourierdlem11  46780  fourierdlem20  46789  fourierdlem21  46790  fourierdlem41  46810  fourierdlem42  46811  fourierdlem48  46816  fourierdlem49  46817  fourierdlem64  46832  fourierdlem71  46839  fourierdlem79  46847  fourierdlem90  46858  fourierdlem91  46859  fourierswlem  46892  etransclem17  46913  etransclem38  46934  saluni  46987  meaiininclem  47148  issmflelem  47406  issmfgtlem  47417  issmfgelem  47431  smflimsuplem4  47485  f1cof1blem  47756  zplusmodne  48031  m1modne  48036  submodneaddmod  48039  nndivides2  48066  sprval  48173  prprval  48208  bgoldbtbndlem2  48516  bgoldbtbndlem3  48517  bgoldbtbnd  48519  isubgrvtxuhgr  48574  isubgredg  48576  grimcnv  48598  isuspgrim  48606  gricushgr  48627  uhgrimisgrgric  48641  grtriclwlk3  48655  isubgr3stgrlem7  48682  grlimgrtri  48713  grlictr  48725  gpgvtx0  48763  gpgvtx1  48764  gpgprismgrusgra  48768  gpgedgvtx1  48772  gpg3kgrtriex  48799  pgnbgreunbgrlem3  48828  pgnbgreunbgrlem6  48834  isclintop  48917  clintopcllaw  48921  nzrneg1ne0  48940  lidldomn1  48941  zlidlring  48944  uzlidlring  48945  2zrngnmlid  48965  cznrng  48971  blenre  49299  blennn  49300  2arymaptf  49377  itcoval1  49388  itcovalendof  49394  ehl2eudisval0  49450  eenglngeehlnmlem2  49463  itsclc0yqsol  49489  inlinecirc02plem  49511  ipolub  49711  ipoglb  49714  nelsubclem  49790  imaid  49877  imaf1co  49878  uptri  49937  uptrar  49939  uptrai  49940  oppc1stflem  50010  setrec2mpt  50420