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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

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

This theorem is used by:  mpidan  701  mpan2  703  biadanid  834  mpjaodan  972  mpjao3dan  1458  mpd3an3  1490  elabd2  3628  eueq2  3672  csbiegf  3885  difsnb  4773  reusv3i  5374  frpoinsg  6344  fimadmfo  6801  fimadmfoALT  6803  fvtresfn  6992  fvmpt3  6994  ffvelcdmd  7080  fnressn  7155  fsnex  7281  f1oiso2  7350  riota5f  7397  onsuc  7807  onsucuni  7822  frrlem10  8290  seqomlem2  8436  oaordi  8529  nnaordi  8602  qsdisj  8790  dom2lem  8987  canth2g  9117  limenpsi  9138  nnfi  9150  php4  9192  onfin  9197  sucxpdom  9219  dmfi  9290  fiin  9380  supiso  9434  ordiso2  9475  wdom2d  9540  elirrvOLD  9558  infeq5  9604  cantnfp1lem3  9647  cantnflem1d  9655  rankwflemb  9763  onenon  9942  cardonle  9950  sdomsdomcardi  9964  acni  10036  cardaleph  10080  djuen  10160  djuinf  10179  infdju1  10180  nnadju  10188  pwsdompw  10193  infdif  10198  cfval  10236  fin34  10380  fin1a2lem1  10390  fin1a2  10405  ttukeylem6  10504  sdomsdomcard  10550  canth3  10551  fpwwe2  10634  canthwelem  10641  gchdju1  10647  pwfseqlem4  10653  gchdjuidm  10659  gchxpidm  10660  tskwe2  10764  rankcf  10768  tskuni  10774  gruxp  10798  dmrecnq  10959  lterpq  10961  archnq  10971  reclem3pr  11040  reclem4pr  11041  0idsr  11088  lep1  12062  ledivp1  12123  negfi  12170  supaddc  12188  supmul1  12190  suprzcl  12682  uz11  12893  zmin  12974  zbtwnre  12976  rpnnen1lem4  13010  rpnnen1lem5  13011  xnegid  13270  supxrre  13359  infxrre  13369  eluzfz2  13566  fzsuc  13606  fzsuc2  13617  fzp1disj  13618  fzneuz  13643  nn0p1elfzo  13738  fllep1  13841  fraclt1  13842  fracle1  13843  fracge0  13844  flhalf  13870  ceige  13884  ceim1l  13887  fldiv  13900  modval  13911  suppssfz  14037  seqeq1  14047  expubnd  14221  iexpcyc  14250  binom2sub1  14264  faclbnd4lem3  14338  pfxid  14729  pfxccatpfx2  14781  swrdccat3blem  14783  cshw0  14838  cshwn  14841  cshimadifsn  14873  cshimadifsn0  14874  pfx2  14991  trclexlem  15038  shftfval  15114  shftcan1  15127  sgnneg  15144  reval  15164  cjmulrcl  15202  addcj  15206  absval  15296  absneg  15335  abscj  15337  sqabsadd  15340  sqabssub  15341  leabs  15357  sqreulem  15418  lo1res  15617  o1of2  15671  o1rlimmul  15677  fsumconst1  15849  flo1  15915  trirecip  15924  efcan  16156  efi4p  16199  resin4p  16200  recos4p  16201  sincossq  16238  ruclem10  16301  iddvds  16333  1dvds  16334  2ebits  16511  lcmftp  16700  coprmgcdb  16713  1idssfct  16744  exprmfct  16769  eulerthlem2  16847  odzphi  16862  pcprendvds  16906  pcmpt  16958  oddprmdvds  16969  vdwlem8  17054  0ram2  17087  prmgaplem7  17123  setsn0fun  17239  setsexstruct2  17241  pwsvscaval  17555  2initoinv  18073  initoeu1  18074  initoeu2lem1  18077  initoeu2  18079  2termoinv  18080  termoeu1  18081  homarel  18099  joinfval  18433  meetfval  18447  latjcom  18509  latmcom  18525  0subm  18882  sgrp2nmndlem5  18997  grprcan  19046  isgrpid2  19049  grpinvid  19072  mulgnn0z  19173  qus0  19266  eqg0subg  19273  ghmker  19318  symgbasmap  19453  symginv  19478  pmtrfrn  19534  odmulg2  19631  slwpgp  19689  pj1eq  19776  efgtf  19798  frgpinv  19840  frgpup2  19852  cnaddablx  19944  cnaddabl  19945  zaddablx  19948  imasabl  19952  dprdfadd  20098  dpjidcl  20136  dpjlid  20139  pgpfac1lem3  20155  omndmul2  20209  omndmul  20211  rngen1zr0  20268  srgen1zr0  20304  1unit  20463  unitgrpid  20474  1rinv  20484  irredn0  20512  irredneg  20519  c0snmgmhm  20551  rngisomring1  20557  zrrnghm  20646  rnrhmsubrg  20715  zrinitorngc  20752  zrtermorngc  20753  zrtermoringc  20785  isdrng2  20854  abv0  20937  abv1z  20938  abvneg  20940  orng0le1  20988  lmodfopne  21032  lsssn0  21080  lspsn0  21140  lsp0  21141  lmhmvsca  21177  lmhmrnlss  21182  lmhmkerlss  21183  lsppratlem5  21286  rsp1  21377  kerlidl  21428  ring2idlqus  21460  rngqiprngfulem4  21465  rngqiprngfu  21468  ssdifidllem  21495  cnfldneg  21559  zringcyg  21630  chrid  21686  chrrhm  21692  ip0r  21798  ocvlss  21833  ocv1  21840  rlmassa  22031  psrbagfsupp  22080  snifpsrbag  22081  psrbaglefi  22087  psrvscaval  22111  psrdi  22125  psrdir  22126  mplvscaval  22176  mhpmpl  22318  mhpdeg  22319  mhppwdeg  22324  psdmul  22340  psdpw  22344  coe1sclmulfv  22455  coe1id  22465  evl1var  22507  mamuvs1  22573  mamuvs2  22574  matecl  22593  matvscacell  22604  mat0scmat  22706  submaval0  22748  mdetrsca  22771  maduval  22806  minmar1val0  22815  pmatcollpw3fi1lem2  22955  chcoeffeqlem  23053  cayleyhamilton0  23057  cayleyhamiltonALT  23059  toponsspwpw  23090  cctop  23174  cldval  23191  ntrfval  23192  clsfval  23193  cmclsopn  23230  opncldf3  23254  neifval  23267  lpfval  23306  cnrmnrm  23529  dis2ndc  23628  islocfin  23685  tx1cn  23777  idqtop  23874  kqtopon  23895  kqid  23896  kqcld  23903  hmphen2  23967  filssufil  24080  ufileu  24087  alexsublem  24212  efmndtmd  24269  symgtgp  24274  ustuqtop4  24412  cstucnd  24451  metustexhalf  24724  nm0  24797  rlmnlm  24856  nmolb  24885  metdseq0  25023  pi1xfrval  25224  clmvneg1  25269  clmvsubval  25279  ipcau2  25404  tcphcphlem1  25405  tcphcphlem2  25406  cmetcaulem  25458  ovolicc2lem3  25689  ovolicc2lem4  25690  mbfmulc2lem  25817  i1fpos  25876  mbfi1fseqlem3  25887  itg2ge0  25905  bddiblnc  26012  dvres2  26082  dvaddbr  26108  dvmulbr  26109  dvcobr  26116  dvfsumlem4  26199  ftc1a  26207  ftc1lem6  26211  uc1pmon1p  26320  ig1pval2  26345  dgradd2  26436  dgrcolem2  26442  plydivlem4  26468  plydiveu  26470  elqaalem3  26493  qaa  26495  ulmdvlem1  26574  abelthlem6  26610  abelthlem7  26612  eflogeq  26778  jensenlem2  27163  harmonicbnd4  27186  sgmnncl  27322  dchrptlem2  27440  1lgs  27515  lgs1  27516  2sqcoprm  27610  addsqnreup  27618  dchrisumlem2  27665  dchrisum0lem2a  27692  selberg2lem  27725  pntrsumo1  27740  pntrsumbnd  27741  pntpbnd1  27761  pntlemr  27777  pntlemj  27778  padicabvf  27806  bdayval  27823  noextendgt  27845  nosupbnd2lem1  27890  noinfbnd2lem1  27905  noetainflem4  27915  oldval  28038  divmuls  28425  divscl  28427  seqsp1  28515  bdayfinbndlem1  28671  zz12s  28679  remulscllem1  28704  symquadprlnglem  28981  plngrotlem2  29081  incistruhgr  29440  subgrprop3  29637  subgruhgredgd  29645  usgrexi  29802  cusgrexi  29804  cusgrsizeinds  29813  vtxdgfusgrf  29858  1hevtxdg1  29867  1egrvtxdg1  29870  ewlkprop  29964  wlklenvm1  29982  wlkl1loop  29998  wlkp1lem4  30035  2pthnloop  30091  upgrclwlkcompim  30141  crctcshwlkn0lem4  30173  crctcshwlkn0lem5  30174  crctcshwlkn0lem6  30175  crctcshwlkn0lem7  30176  crctcshlem4  30180  wspthnonp  30219  wlkswwlksf1o  30239  wwlksnwwlksnon  30275  umgr2wlkon  30310  wwlks2onv  30313  elwwlks2ons3im  30314  elwspths2spth  30330  umgrclwwlkge2  30353  clwlkclwwlkf1lem3  30368  erclwwlkref  30382  clwwlknp  30399  wwlksext2clwwlk  30419  wwlksubclwwlk  30420  0pthon1  30490  1wlkdlem4  30502  1pthd  30505  3spthd  30538  eupth2eucrct  30579  eucrctshift  30605  eucrct2eupth  30607  frgrncvvdeqlem8  30668  frgr2wwlkeqm  30693  isgrpoi  30861  grpoinvfval  30885  grpodivfval  30897  vcz  30938  cnaddabloOLD  30944  nvz0  31031  sspz  31098  lno0  31119  nmobndi  31138  ipasslem2  31195  shunssi  31731  ococin  31771  ssjo  31810  pjocini  32061  nlfnval  32244  lncnopbd  32400  riesz3i  32425  cnlnadjlem7  32436  pjclem4  32562  pj3si  32570  hstoc  32585  hstnmoc  32586  hstoh  32595  hst0  32596  mdsl2i  32685  chirredlem3  32755  chirredlem4  32756  dmdbr5ati  32785  rexunirn  32849  fcnvgreu  33028  infxrge0glb  33121  cycpmco2lem5  33459  cycpmco2lem6  33460  cycpmco2lem7  33461  isarchi3  33516  rlocisunit  33605  nsgqusf1olem2  33732  ssmxidllem  33765  rprmdvdspow  33832  ressply1sub  33869  selvply1rhmlemb  33918  fedgmullem1  34028  extdg1id  34065  nn0constr  34160  zartopn  34274  zarcmplem  34280  esumcvg  34485  esumcvgre  34490  sigaval  34510  unelldsys  34557  fiunelros  34573  measval  34597  pmeasmono  34723  probfinmeasb  34827  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemsi  34914  ballotlemfrci  34927  signlem0  34983  breprexp  35029  bnj1006  35357  bnj1110  35379  bnj1253  35414  bnj1280  35417  bnj1463  35452  bnj1312  35455  scottrankeqel  35526  fineqvinfep  35546  erdszelem7  35697  erdszelem8  35698  cvmliftlem10  35794  cvmliftlem13  35796  cvmlift2lem9  35811  cvmlift3lem6  35824  cvmlift3lem7  35825  cvmlift3lem9  35827  satfv1lem  35862  dfrdg2  36293  cldregopn  36870  tailfval  36911  filnetlem3  36919  filnetlem4  36920  ontopbas  36967  bj-nnfbd  37422  bj-elid4  37840  bj-imdiridlem  37857  f1omptsnlem  38010  icoreunrn  38033  relowlpssretop  38038  fvineqsnf1  38084  wl-sbal2  38247  unccur  38282  poimirlem1  38300  poimirlem2  38301  poimirlem4  38303  poimirlem6  38305  poimirlem7  38306  poimirlem11  38310  poimirlem12  38311  poimirlem17  38316  poimirlem20  38319  poimirlem22  38321  poimirlem23  38322  poimirlem28  38327  poimir  38332  ismblfin  38340  cnambfre  38347  ftc1cnnc  38371  dvasin  38383  ismtyres  38487  heiborlem8  38497  ghomidOLD  38568  rngosn6  38605  rngonegmn1l  38620  rngonegmn1r  38621  rngoneglmul  38622  rngonegrmul  38623  idlnegcl  38701  0idl  38704  0rngo  38706  smprngopr  38731  sucmapsuc  39166  cossex  39186  qsdisjALTV  39376  cnvepresdmqss  39414  mpets2  39632  lkrval  39890  ldualvaddval  39933  ldualvsval  39940  opoc1  40004  pmap0  40567  pmap1N  40569  pexmidALTN  40780  cdleme31fv  41192  cdlemg27b  41498  erngdvlem4  41793  erng0g  41796  erngdvlem4-rN  41801  dvalveclem  41827  dvh0g  41913  dih0cnv  42085  dih1rn  42089  dih1cnv  42090  doch0  42160  doch1  42161  lcfl7lem  42301  mapdheq  42530  hdmap1eq  42603  hdmapval2lem  42633  hgmapvvlem3  42727  zndvdchrrhm  42768  lcmineqlem13  42836  aks4d1p9  42883  primrootsunit1  42892  aks6d1c1p1  42902  aks6d1c1p6  42909  aks6d1c1p8  42910  sticksstones1  42941  sticksstones6  42946  sticksstones7  42947  sticksstones11  42951  sticksstones12a  42952  sticksstones12  42953  sticksstones22  42963  aks6d1c6isolem1  42969  aks6d1c6isolem2  42970  unitscyglem5  42994  renegid  43162  sn-0ne2  43195  remul01  43196  remulinvcom  43222  sn-0tie0  43253  renegmulnnass  43267  domnexpgn0cl  43319  abvexp  43328  frlmsnic  43336  fsuppssind  43353  mzpval  43491  mzpindd  43505  pellex  43590  2nn0ind  43700  jm2.26lem3  43756  pw2f1o2val  43794  wepwsolem  43797  fnwe2lem3  43807  lnmfg  43837  dgrsub2  43890  mpaaeu  43905  flcidc  43925  dflim5  44084  naddwordnexlem1  44152  rtrclexlem  44370  cnvrcl0  44379  brcoffn  44784  clsk1indlem3  44797  clsneif1o  44858  clsneicnv  44859  clsneikex  44860  clsneinex  44861  neicvgmex  44871  neicvgel1  44873  suprleubrd  44920  suprlubrd  44922  imo72b2  44926  dvconstbi  45072  bcc0  45078  binomcxplemnotnn0  45094  nnfoctb  45796  infleinflem1  46113  fprodcnlem  46343  sumnnodd  46374  icccncfext  46629  itgsin0pilem1  46692  stoweidlem32  46774  stoweidlem35  46777  stoweidlem36  46778  stoweidlem37  46779  stoweidlem43  46785  stoweidlem50  46792  wallispilem5  46811  stirlinglem2  46817  stirlinglem3  46818  stirlinglem4  46819  stirlinglem8  46823  stirlinglem11  46826  stirlinglem12  46827  stirlinglem14  46829  stirlinglem15  46830  fourierdlem11  46860  fourierdlem20  46869  fourierdlem21  46870  fourierdlem41  46890  fourierdlem42  46891  fourierdlem48  46896  fourierdlem49  46897  fourierdlem64  46912  fourierdlem71  46919  fourierdlem79  46927  fourierdlem90  46938  fourierdlem91  46939  fourierswlem  46972  etransclem17  46993  etransclem38  47014  saluni  47067  meaiininclem  47228  issmflelem  47486  issmfgtlem  47497  issmfgelem  47511  smflimsuplem4  47565  f1cof1blem  47839  zplusmodne  48114  m1modne  48119  submodneaddmod  48122  nndivides2  48149  sprval  48256  prprval  48291  bgoldbtbndlem2  48599  bgoldbtbndlem3  48600  bgoldbtbnd  48602  isubgrvtxuhgr  48657  isubgredg  48659  grimcnv  48681  isuspgrim  48689  gricushgr  48710  uhgrimisgrgric  48724  grtriclwlk3  48738  isubgr3stgrlem7  48765  grlimgrtri  48796  grlictr  48808  gpgvtx0  48846  gpgvtx1  48847  gpgprismgrusgra  48851  gpgedgvtx1  48855  gpg3kgrtriex  48882  pgnbgreunbgrlem3  48911  pgnbgreunbgrlem6  48917  isclintop  49000  clintopcllaw  49004  nzrneg1ne0  49023  lidldomn1  49024  zlidlring  49027  uzlidlring  49028  2zrngnmlid  49048  cznrng  49054  blenre  49382  blennn  49383  2arymaptf  49460  itcoval1  49471  itcovalendof  49477  ehl2eudisval0  49533  eenglngeehlnmlem2  49546  itsclc0yqsol  49572  inlinecirc02plem  49594  ipolub  49794  ipoglb  49797  nelsubclem  49873  imaid  49960  imaf1co  49961  uptri  50020  uptrar  50022  uptrai  50023  oppc1stflem  50093  setrec2mpt  50503