Theorem mpdan 686

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 22	. 2 ⊢ (𝜑 → 𝜑)
2		mpdan.1	. 2 ⊢ (𝜑 → 𝜓)
3		mpdan.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  mpidan  688  mpan2  690  biadanid  822  mpjaodan  958  mpjao3dan  1432  mpd3an3  1463  elabd2  3661  eueq2  3707  csbiegf  3928  difsnb  4810  reusv3i  5403  frpoinsg  6345  fimadmfo  6815  fimadmfoALT  6817  fvtresfn  7001  fvmpt3  7003  ffvelcdmd  7088  fnressn  7156  fsnex  7281  f1oiso2  7349  riota5f  7394  onsuc  7799  onsucuni  7816  frrlem10  8280  seqomlem2  8451  oaordi  8546  nnaordi  8618  qsdisj  8788  dom2lem  8988  canth2g  9131  limenpsi  9152  nnfi  9167  php4  9213  onfin  9230  sucxpdom  9255  xpfiOLD  9318  dmfi  9330  pwfilemOLD  9346  pwfiOLD  9347  fiin  9417  supiso  9470  ordiso2  9510  wdom2d  9575  infeq5  9632  cantnfp1lem3  9675  cantnflem1d  9683  rankwflemb  9788  onenon  9944  cardonle  9952  sdomsdomcardi  9966  acni  10040  cardaleph  10084  djuen  10164  djuinf  10183  infdju1  10184  nnadju  10192  pwsdompw  10199  infdif  10204  cfval  10242  fin34  10385  fin1a2lem1  10395  fin1a2  10410  ttukeylem6  10509  sdomsdomcard  10555  canth3  10556  fpwwe2  10638  canthwelem  10645  gchdju1  10651  pwfseqlem4  10657  gchdjuidm  10663  gchxpidm  10664  tskwe2  10768  rankcf  10772  tskuni  10778  gruxp  10802  dmrecnq  10963  lterpq  10965  archnq  10975  reclem3pr  11044  reclem4pr  11045  0idsr  11092  lep1  12055  ledivp1  12116  negfi  12163  supaddc  12181  supmul1  12183  suprzcl  12642  uz11  12847  zmin  12928  zbtwnre  12930  rpnnen1lem4  12964  rpnnen1lem5  12965  xnegid  13217  supxrre  13306  infxrre  13315  eluzfz2  13509  fzsuc  13548  fzsuc2  13559  fzp1disj  13560  fzneuz  13582  nn0p1elfzo  13675  fllep1  13766  fraclt1  13767  fracle1  13768  fracge0  13769  flhalf  13795  ceige  13809  ceim1l  13812  fldiv  13825  modval  13836  suppssfz  13959  seqeq1  13969  expubnd  14142  iexpcyc  14171  binom2sub1  14184  faclbnd4lem3  14255  pfxid  14634  pfxccatpfx2  14687  swrdccat3blem  14689  cshw0  14744  cshwn  14747  cshimadifsn  14780  cshimadifsn0  14781  pfx2  14898  trclexlem  14941  shftfval  15017  shftcan1  15030  reval  15053  cjmulrcl  15091  addcj  15095  absval  15185  absneg  15224  abscj  15226  sqabsadd  15229  sqabssub  15230  leabs  15246  sqreulem  15306  lo1res  15503  o1of2  15557  o1rlimmul  15563  flo1  15800  trirecip  15809  efcan  16039  efi4p  16080  resin4p  16081  recos4p  16082  sincossq  16119  ruclem10  16182  iddvds  16213  1dvds  16214  2ebits  16388  lcmftp  16573  coprmgcdb  16586  1idssfct  16617  exprmfct  16641  eulerthlem2  16715  odzphi  16729  pcprendvds  16773  pcmpt  16825  oddprmdvds  16836  vdwlem8  16921  0ram2  16954  prmgaplem7  16990  setsn0fun  17106  setsexstruct2  17108  pwsvscaval  17441  2initoinv  17960  initoeu1  17961  initoeu2lem1  17964  initoeu2  17966  2termoinv  17967  termoeu1  17968  homarel  17986  joinfval  18326  meetfval  18340  latjcom  18400  latmcom  18416  0subm  18698  sgrp2nmndlem5  18810  grprcan  18858  isgrpid2  18861  grpinvid  18884  mulgnn0z  18981  0subgOLD  19032  qus0  19068  eqg0subg  19073  ghmker  19118  symgbasmap  19244  symginv  19270  pmtrfrn  19326  odmulg2  19423  slwpgp  19481  pj1eq  19568  efgtf  19590  frgpinv  19632  frgpup2  19644  cnaddablx  19736  cnaddabl  19737  zaddablx  19740  imasabl  19744  dprdfadd  19890  dpjidcl  19928  dpjlid  19931  pgpfac1lem3  19947  srgen1zr  20039  1unit  20188  unitgrpid  20199  1rinv  20209  irredn0  20237  irredneg  20244  rnrhmsubrg  20352  isdrng2  20371  ringen1zr  20399  abv0  20439  abv1z  20440  abvneg  20442  lmodfopne  20510  lsssn0  20558  lspsn0  20619  lsp0  20620  lmhmvsca  20656  lmhmrnlss  20661  lmhmkerlss  20662  lsppratlem5  20764  rsp1  20849  cnfldneg  20971  zringcyg  21039  chrid  21079  chrrhm  21083  ip0r  21190  ocvlss  21225  ocv1  21232  rlmassa  21425  psrbagfsupp  21473  snifpsrbag  21475  psrbaglefi  21485  psrvscaval  21511  psrdi  21526  psrdir  21527  mplvscaval  21575  mhpmpl  21687  mhpdeg  21688  mhppwdeg  21693  coe1sclmulfv  21805  ply1idvr1  21817  evl1var  21855  mamuvs1  21905  mamuvs2  21906  matecl  21927  matvscacell  21938  mat0scmat  22040  submaval0  22082  mdetrsca  22105  maduval  22140  minmar1val0  22149  pmatcollpw3fi1lem2  22289  chcoeffeqlem  22387  cayleyhamilton0  22391  cayleyhamiltonALT  22393  toponsspwpw  22424  cctop  22509  cldval  22527  ntrfval  22528  clsfval  22529  cmclsopn  22566  opncldf3  22590  neifval  22603  lpfval  22642  cnrmnrm  22865  dis2ndc  22964  islocfin  23021  tx1cn  23113  idqtop  23210  kqtopon  23231  kqid  23232  kqcld  23239  hmphen2  23303  filssufil  23416  ufileu  23423  alexsublem  23548  efmndtmd  23605  symgtgp  23610  ustuqtop4  23749  cstucnd  23789  metustexhalf  24065  nm0  24138  rlmnlm  24205  nmolb  24234  metdseq0  24370  pi1xfrval  24570  clmvneg1  24615  clmvsubval  24625  ipcau2  24751  tcphcphlem1  24752  tcphcphlem2  24753  cmetcaulem  24805  ovolicc2lem3  25036  ovolicc2lem4  25037  mbfmulc2lem  25164  i1fpos  25224  mbfi1fseqlem3  25235  itg2ge0  25253  bddiblnc  25359  dvres2  25429  dvaddbr  25455  dvmulbr  25456  dvcobr  25463  dvfsumlem4  25546  ftc1a  25554  ftc1lem6  25558  uc1pmon1p  25669  ig1pval2  25691  dgradd2  25782  dgrcolem2  25788  plydivlem4  25809  plydiveu  25811  elqaalem3  25834  qaa  25836  ulmdvlem1  25912  abelthlem6  25948  abelthlem7  25950  eflogeq  26110  jensenlem2  26492  harmonicbnd4  26515  sgmnncl  26651  dchrptlem2  26768  1lgs  26843  lgs1  26844  2sqcoprm  26938  addsqnreup  26946  dchrisumlem2  26993  dchrisum0lem2a  27020  selberg2lem  27053  pntrsumo1  27068  pntrsumbnd  27069  pntpbnd1  27089  pntlemr  27105  pntlemj  27106  padicabvf  27134  bdayval  27151  noextendgt  27173  nosupbnd2lem1  27218  noinfbnd2lem1  27233  noetainflem4  27243  oldval  27349  divsmul  27667  divscl  27669  incistruhgr  28339  subgrprop3  28533  subgruhgredgd  28541  usgrexi  28698  cusgrexi  28700  cusgrsizeinds  28709  vtxdgfusgrf  28754  1hevtxdg1  28763  1egrvtxdg1  28766  ewlkprop  28860  wlklenvm1  28879  wlkl1loop  28895  wlkp1lem4  28933  2pthnloop  28988  upgrclwlkcompim  29038  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  crctcshwlkn0lem6  29069  crctcshwlkn0lem7  29070  crctcshlem4  29074  wspthnonp  29113  wlkswwlksf1o  29133  wwlksnwwlksnon  29169  umgr2wlkon  29204  wwlks2onv  29207  elwwlks2ons3im  29208  elwspths2spth  29221  umgrclwwlkge2  29244  clwlkclwwlkf1lem3  29259  erclwwlkref  29273  clwwlknp  29290  wwlksext2clwwlk  29310  wwlksubclwwlk  29311  0pthon1  29381  1wlkdlem4  29393  1pthd  29396  3spthd  29429  eupth2eucrct  29470  eucrctshift  29496  eucrct2eupth  29498  frgrncvvdeqlem8  29559  frgr2wwlkeqm  29584  isgrpoi  29751  grpoinvfval  29775  grpodivfval  29787  vcz  29828  cnaddabloOLD  29834  nvz0  29921  sspz  29988  lno0  30009  nmobndi  30028  ipasslem2  30085  shunssi  30621  ococin  30661  ssjo  30700  pjocini  30951  nlfnval  31134  lncnopbd  31290  riesz3i  31315  cnlnadjlem7  31326  pjclem4  31452  pj3si  31460  hstoc  31475  hstnmoc  31476  hstoh  31485  hst0  31486  mdsl2i  31575  chirredlem3  31645  chirredlem4  31646  dmdbr5ati  31675  rexunirn  31732  fcnvgreu  31898  infxrge0glb  31978  omndmul2  32230  omndmul  32232  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2lem7  32291  isarchi3  32333  orng0le1  32430  nsgqusf1olem2  32525  kerlidl  32538  ssmxidllem  32589  ressply1sub  32659  fedgmullem1  32714  extdg1id  32742  zartopn  32855  zarcmplem  32861  esumcvg  33084  esumcvgre  33089  sigaval  33109  unelldsys  33156  fiunelros  33172  measval  33196  pmeasmono  33323  probfinmeasb  33427  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemsi  33513  ballotlemfrci  33526  sgnneg  33539  signlem0  33598  breprexp  33645  bnj1006  33971  bnj1110  33993  bnj1253  34028  bnj1280  34031  bnj1463  34066  bnj1312  34069  erdszelem7  34188  erdszelem8  34189  cvmliftlem10  34285  cvmliftlem13  34287  cvmlift2lem9  34302  cvmlift3lem6  34315  cvmlift3lem7  34316  cvmlift3lem9  34318  satfv1lem  34353  dfrdg2  34767  gg-dvmulbr  35175  gg-dvcobr  35176  cldregopn  35216  tailfval  35257  filnetlem3  35265  filnetlem4  35266  ontopbas  35313  bj-elid4  36049  bj-imdiridlem  36066  f1omptsnlem  36217  icoreunrn  36240  relowlpssretop  36245  fvineqsnf1  36291  wl-sbal2  36429  unccur  36471  poimirlem1  36489  poimirlem2  36490  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem11  36499  poimirlem12  36500  poimirlem17  36505  poimirlem20  36508  poimirlem22  36510  poimirlem23  36511  poimirlem28  36516  poimir  36521  ismblfin  36529  cnambfre  36536  ftc1cnnc  36560  dvasin  36572  ismtyres  36676  heiborlem8  36686  ghomidOLD  36757  rngosn6  36794  rngonegmn1l  36809  rngonegmn1r  36810  rngoneglmul  36811  rngonegrmul  36812  idlnegcl  36890  0idl  36893  0rngo  36895  smprngopr  36920  cossex  37289  qsdisjALTV  37485  cnvepresdmqss  37522  mpets2  37711  lkrval  37958  ldualvaddval  38001  ldualvsval  38008  opoc1  38072  pmap0  38636  pmap1N  38638  pexmidALTN  38849  cdleme31fv  39261  cdlemg27b  39567  erngdvlem4  39862  erng0g  39865  erngdvlem4-rN  39870  dvalveclem  39896  dvh0g  39982  dih0cnv  40154  dih1rn  40158  dih1cnv  40159  doch0  40229  doch1  40230  lcfl7lem  40370  mapdheq  40599  hdmap1eq  40672  hdmapval2lem  40702  hgmapvvlem3  40796  lcmineqlem13  40906  aks4d1p9  40953  sticksstones1  40962  sticksstones6  40967  sticksstones7  40968  sticksstones11  40972  sticksstones12a  40973  sticksstones12  40974  sticksstones22  40984  frlmsnic  41110  fsuppssind  41165  renegid  41246  sn-0ne2  41279  remul01  41280  remulinvcom  41305  sn-0tie0  41312  renegmulnnass  41326  sn-inelr  41338  mzpval  41470  mzpindd  41484  pellex  41573  2nn0ind  41684  jm2.26lem3  41740  pw2f1o2val  41778  wepwsolem  41784  fnwe2lem3  41794  lnmfg  41824  dgrsub2  41877  mpaaeu  41892  flcidc  41916  dflim5  42079  naddwordnexlem1  42148  rtrclexlem  42367  cnvrcl0  42376  brcoffn  42781  clsk1indlem3  42794  clsneif1o  42855  clsneicnv  42856  clsneikex  42857  clsneinex  42858  neicvgmex  42868  neicvgel1  42870  suprleubrd  42918  suprlubrd  42920  imo72b2  42924  dvconstbi  43093  bcc0  43099  binomcxplemnotnn0  43115  nnfoctb  43734  infleinflem1  44080  fprodcnlem  44315  sumnnodd  44346  icccncfext  44603  itgsin0pilem1  44666  stoweidlem32  44748  stoweidlem35  44751  stoweidlem36  44752  stoweidlem37  44753  stoweidlem43  44759  stoweidlem50  44766  wallispilem5  44785  stirlinglem2  44791  stirlinglem3  44792  stirlinglem4  44793  stirlinglem8  44797  stirlinglem11  44800  stirlinglem12  44801  stirlinglem14  44803  stirlinglem15  44804  fourierdlem11  44834  fourierdlem20  44843  fourierdlem21  44844  fourierdlem41  44864  fourierdlem42  44865  fourierdlem48  44870  fourierdlem49  44871  fourierdlem64  44886  fourierdlem71  44893  fourierdlem79  44901  fourierdlem90  44912  fourierdlem91  44913  fourierswlem  44946  etransclem17  44967  etransclem38  44988  saluni  45041  meaiininclem  45202  issmflelem  45460  issmfgtlem  45471  issmfgelem  45485  smflimsuplem4  45539  f1cof1blem  45784  sprval  46147  prprval  46182  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbnd  46477  isomushgr  46494  isomuspgrlem1  46495  isclintop  46617  clintopcllaw  46621  nzrneg1ne0  46643  c0snmgmhm  46713  zrrnghm  46716  rngisomring1  46720  ring2idlqus  46794  rngqiprngfulem4  46799  rngqiprngfu  46802  lidldomn1  46823  zlidlring  46826  uzlidlring  46827  2zrngnmlid  46847  cznrng  46853  zrinitorngc  46898  zrtermorngc  46899  zrtermoringc  46968  coe1id  47065  blenre  47260  blennn  47261  2arymaptf  47338  itcoval1  47349  itcovalendof  47355  ehl2eudisval0  47411  eenglngeehlnmlem2  47424  itsclc0yqsol  47450  inlinecirc02plem  47472  ipolub  47613  ipoglb  47616  setrec2mpt  47742