Theorem mpdan 685

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  mpidan  687  mpan2  689  biadanid  821  mpjaodan  956  mpjao3dan  1429  mpd3an3  1459  elabd2  3657  eueq2  3704  csbiegf  3926  difsnb  4815  reusv3i  5408  frpoinsg  6356  fimadmfo  6824  fimadmfoALT  6826  fvtresfn  7011  fvmpt3  7013  ffvelcdmd  7099  fnressn  7172  fsnex  7297  f1oiso2  7364  riota5f  7409  onsuc  7820  onsucuni  7837  frrlem10  8310  seqomlem2  8481  oaordi  8576  nnaordi  8648  qsdisj  8823  dom2lem  9023  canth2g  9169  limenpsi  9190  nnfi  9205  php4  9247  onfin  9264  sucxpdom  9289  xpfiOLD  9361  dmfi  9377  pwfilemOLD  9390  pwfiOLD  9391  fiin  9465  supiso  9518  ordiso2  9558  wdom2d  9623  infeq5  9680  cantnfp1lem3  9723  cantnflem1d  9731  rankwflemb  9836  onenon  9992  cardonle  10000  sdomsdomcardi  10014  acni  10088  cardaleph  10132  djuen  10212  djuinf  10231  infdju1  10232  nnadju  10240  pwsdompw  10247  infdif  10252  cfval  10290  fin34  10433  fin1a2lem1  10443  fin1a2  10458  ttukeylem6  10557  sdomsdomcard  10603  canth3  10604  fpwwe2  10686  canthwelem  10693  gchdju1  10699  pwfseqlem4  10705  gchdjuidm  10711  gchxpidm  10712  tskwe2  10816  rankcf  10820  tskuni  10826  gruxp  10850  dmrecnq  11011  lterpq  11013  archnq  11023  reclem3pr  11092  reclem4pr  11093  0idsr  11140  lep1  12106  ledivp1  12168  negfi  12215  supaddc  12233  supmul1  12235  suprzcl  12694  uz11  12899  zmin  12980  zbtwnre  12982  rpnnen1lem4  13016  rpnnen1lem5  13017  xnegid  13271  supxrre  13360  infxrre  13369  eluzfz2  13563  fzsuc  13602  fzsuc2  13613  fzp1disj  13614  fzneuz  13636  nn0p1elfzo  13729  fllep1  13821  fraclt1  13822  fracle1  13823  fracge0  13824  flhalf  13850  ceige  13864  ceim1l  13867  fldiv  13880  modval  13891  suppssfz  14014  seqeq1  14024  expubnd  14196  iexpcyc  14225  binom2sub1  14238  faclbnd4lem3  14312  pfxid  14692  pfxccatpfx2  14745  swrdccat3blem  14747  cshw0  14802  cshwn  14805  cshimadifsn  14838  cshimadifsn0  14839  pfx2  14956  trclexlem  14999  shftfval  15075  shftcan1  15088  reval  15111  cjmulrcl  15149  addcj  15153  absval  15243  absneg  15282  abscj  15284  sqabsadd  15287  sqabssub  15288  leabs  15304  sqreulem  15364  lo1res  15561  o1of2  15615  o1rlimmul  15621  flo1  15858  trirecip  15867  efcan  16098  efi4p  16139  resin4p  16140  recos4p  16141  sincossq  16178  ruclem10  16241  iddvds  16272  1dvds  16273  2ebits  16447  lcmftp  16637  coprmgcdb  16650  1idssfct  16681  exprmfct  16705  eulerthlem2  16784  odzphi  16798  pcprendvds  16842  pcmpt  16894  oddprmdvds  16905  vdwlem8  16990  0ram2  17023  prmgaplem7  17059  setsn0fun  17175  setsexstruct2  17177  pwsvscaval  17510  2initoinv  18032  initoeu1  18033  initoeu2lem1  18036  initoeu2  18038  2termoinv  18039  termoeu1  18040  homarel  18058  joinfval  18398  meetfval  18412  latjcom  18472  latmcom  18488  0subm  18807  sgrp2nmndlem5  18919  grprcan  18968  isgrpid2  18971  grpinvid  18994  mulgnn0z  19095  0subgOLD  19146  qus0  19183  eqg0subg  19190  ghmker  19236  symgbasmap  19374  symginv  19400  pmtrfrn  19456  odmulg2  19553  slwpgp  19611  pj1eq  19698  efgtf  19720  frgpinv  19762  frgpup2  19774  cnaddablx  19866  cnaddabl  19867  zaddablx  19870  imasabl  19874  dprdfadd  20020  dpjidcl  20058  dpjlid  20061  pgpfac1lem3  20077  srgen1zr  20199  1unit  20356  unitgrpid  20367  1rinv  20377  irredn0  20405  irredneg  20412  c0snmgmhm  20444  rngisomring1  20450  zrrnghm  20518  rnrhmsubrg  20589  zrinitorngc  20620  zrtermorngc  20621  zrtermoringc  20653  isdrng2  20721  ringen1zr  20757  abv0  20802  abv1z  20803  abvneg  20805  lmodfopne  20876  lsssn0  20925  lspsn0  20985  lsp0  20986  lmhmvsca  21023  lmhmrnlss  21028  lmhmkerlss  21029  lsppratlem5  21132  rsp1  21226  kerlidl  21267  ring2idlqus  21298  rngqiprngfulem4  21303  rngqiprngfu  21306  cnfldneg  21387  zringcyg  21459  chrid  21519  chrrhm  21525  ip0r  21633  ocvlss  21668  ocv1  21675  rlmassa  21868  psrbagfsupp  21917  snifpsrbag  21919  psrbaglefi  21929  psrvscaval  21959  psrdi  21974  psrdir  21975  mplvscaval  22025  mhpmpl  22138  mhpdeg  22139  mhppwdeg  22144  psdmul  22160  coe1sclmulfv  22274  ply1idvr1  22286  evl1var  22327  mamuvs1  22396  mamuvs2  22397  matecl  22418  matvscacell  22429  mat0scmat  22531  submaval0  22573  mdetrsca  22596  maduval  22631  minmar1val0  22640  pmatcollpw3fi1lem2  22780  chcoeffeqlem  22878  cayleyhamilton0  22882  cayleyhamiltonALT  22884  toponsspwpw  22915  cctop  23000  cldval  23018  ntrfval  23019  clsfval  23020  cmclsopn  23057  opncldf3  23081  neifval  23094  lpfval  23133  cnrmnrm  23356  dis2ndc  23455  islocfin  23512  tx1cn  23604  idqtop  23701  kqtopon  23722  kqid  23723  kqcld  23730  hmphen2  23794  filssufil  23907  ufileu  23914  alexsublem  24039  efmndtmd  24096  symgtgp  24101  ustuqtop4  24240  cstucnd  24280  metustexhalf  24556  nm0  24629  rlmnlm  24696  nmolb  24725  metdseq0  24861  pi1xfrval  25072  clmvneg1  25117  clmvsubval  25127  ipcau2  25253  tcphcphlem1  25254  tcphcphlem2  25255  cmetcaulem  25307  ovolicc2lem3  25539  ovolicc2lem4  25540  mbfmulc2lem  25667  i1fpos  25727  mbfi1fseqlem3  25738  itg2ge0  25756  bddiblnc  25862  dvres2  25932  dvaddbr  25959  dvmulbr  25960  dvmulbrOLD  25961  dvcobr  25968  dvcobrOLD  25969  dvfsumlem4  26055  ftc1a  26063  ftc1lem6  26067  uc1pmon1p  26179  ig1pval2  26204  dgradd2  26296  dgrcolem2  26302  plydivlem4  26324  plydiveu  26326  elqaalem3  26349  qaa  26351  ulmdvlem1  26429  abelthlem6  26466  abelthlem7  26468  eflogeq  26629  jensenlem2  27016  harmonicbnd4  27039  sgmnncl  27175  dchrptlem2  27294  1lgs  27369  lgs1  27370  2sqcoprm  27464  addsqnreup  27472  dchrisumlem2  27519  dchrisum0lem2a  27546  selberg2lem  27579  pntrsumo1  27594  pntrsumbnd  27595  pntpbnd1  27615  pntlemr  27631  pntlemj  27632  padicabvf  27660  bdayval  27678  noextendgt  27700  nosupbnd2lem1  27745  noinfbnd2lem1  27760  noetainflem4  27770  oldval  27878  divsmul  28220  divscl  28222  seqsp1  28285  remulscllem1  28351  incistruhgr  29015  subgrprop3  29212  subgruhgredgd  29220  usgrexi  29377  cusgrexi  29379  cusgrsizeinds  29389  vtxdgfusgrf  29434  1hevtxdg1  29443  1egrvtxdg1  29446  ewlkprop  29540  wlklenvm1  29559  wlkl1loop  29575  wlkp1lem4  29613  2pthnloop  29668  upgrclwlkcompim  29718  crctcshwlkn0lem4  29747  crctcshwlkn0lem5  29748  crctcshwlkn0lem6  29749  crctcshwlkn0lem7  29750  crctcshlem4  29754  wspthnonp  29793  wlkswwlksf1o  29813  wwlksnwwlksnon  29849  umgr2wlkon  29884  wwlks2onv  29887  elwwlks2ons3im  29888  elwspths2spth  29901  umgrclwwlkge2  29924  clwlkclwwlkf1lem3  29939  erclwwlkref  29953  clwwlknp  29970  wwlksext2clwwlk  29990  wwlksubclwwlk  29991  0pthon1  30061  1wlkdlem4  30073  1pthd  30076  3spthd  30109  eupth2eucrct  30150  eucrctshift  30176  eucrct2eupth  30178  frgrncvvdeqlem8  30239  frgr2wwlkeqm  30264  isgrpoi  30431  grpoinvfval  30455  grpodivfval  30467  vcz  30508  cnaddabloOLD  30514  nvz0  30601  sspz  30668  lno0  30689  nmobndi  30708  ipasslem2  30765  shunssi  31301  ococin  31341  ssjo  31380  pjocini  31631  nlfnval  31814  lncnopbd  31970  riesz3i  31995  cnlnadjlem7  32006  pjclem4  32132  pj3si  32140  hstoc  32155  hstnmoc  32156  hstoh  32165  hst0  32166  mdsl2i  32255  chirredlem3  32325  chirredlem4  32326  dmdbr5ati  32355  rexunirn  32420  fcnvgreu  32590  infxrge0glb  32669  omndmul2  32947  omndmul  32949  cycpmco2lem5  33008  cycpmco2lem6  33009  cycpmco2lem7  33010  isarchi3  33052  orng0le1  33190  nsgqusf1olem2  33289  ssdifidllem  33331  ssmxidllem  33348  rprmdvdspow  33408  ressply1sub  33442  fedgmullem1  33524  extdg1id  33552  zartopn  33690  zarcmplem  33696  esumcvg  33919  esumcvgre  33924  sigaval  33944  unelldsys  33991  fiunelros  34007  measval  34031  pmeasmono  34158  probfinmeasb  34262  ballotlemfc0  34326  ballotlemfcc  34327  ballotlemsi  34348  ballotlemfrci  34361  sgnneg  34374  signlem0  34433  breprexp  34479  bnj1006  34805  bnj1110  34827  bnj1253  34862  bnj1280  34865  bnj1463  34900  bnj1312  34903  erdszelem7  35025  erdszelem8  35026  cvmliftlem10  35122  cvmliftlem13  35124  cvmlift2lem9  35139  cvmlift3lem6  35152  cvmlift3lem7  35153  cvmlift3lem9  35155  satfv1lem  35190  dfrdg2  35619  cldregopn  36043  tailfval  36084  filnetlem3  36092  filnetlem4  36093  ontopbas  36140  bj-elid4  36875  bj-imdiridlem  36892  f1omptsnlem  37043  icoreunrn  37066  relowlpssretop  37071  fvineqsnf1  37117  wl-sbal2  37259  unccur  37304  poimirlem1  37322  poimirlem2  37323  poimirlem4  37325  poimirlem6  37327  poimirlem7  37328  poimirlem11  37332  poimirlem12  37333  poimirlem17  37338  poimirlem20  37341  poimirlem22  37343  poimirlem23  37344  poimirlem28  37349  poimir  37354  ismblfin  37362  cnambfre  37369  ftc1cnnc  37393  dvasin  37405  ismtyres  37509  heiborlem8  37519  ghomidOLD  37590  rngosn6  37627  rngonegmn1l  37642  rngonegmn1r  37643  rngoneglmul  37644  rngonegrmul  37645  idlnegcl  37723  0idl  37726  0rngo  37728  smprngopr  37753  cossex  38117  qsdisjALTV  38313  cnvepresdmqss  38350  mpets2  38539  lkrval  38786  ldualvaddval  38829  ldualvsval  38836  opoc1  38900  pmap0  39464  pmap1N  39466  pexmidALTN  39677  cdleme31fv  40089  cdlemg27b  40395  erngdvlem4  40690  erng0g  40693  erngdvlem4-rN  40698  dvalveclem  40724  dvh0g  40810  dih0cnv  40982  dih1rn  40986  dih1cnv  40987  doch0  41057  doch1  41058  lcfl7lem  41198  mapdheq  41427  hdmap1eq  41500  hdmapval2lem  41530  hgmapvvlem3  41624  zndvdchrrhm  41669  lcmineqlem13  41740  aks4d1p9  41787  primrootsunit1  41795  aks6d1c1p1  41805  aks6d1c1p6  41812  aks6d1c1p8  41813  sticksstones1  41844  sticksstones6  41849  sticksstones7  41850  sticksstones11  41854  sticksstones12a  41855  sticksstones12  41856  sticksstones22  41866  aks6d1c6isolem1  41872  aks6d1c6isolem2  41873  frlmsnic  42012  fsuppssind  42065  renegid  42153  sn-0ne2  42186  remul01  42187  remulinvcom  42212  sn-0tie0  42219  renegmulnnass  42233  sn-inelr  42247  mzpval  42389  mzpindd  42403  pellex  42492  2nn0ind  42603  jm2.26lem3  42659  pw2f1o2val  42697  wepwsolem  42703  fnwe2lem3  42713  lnmfg  42743  dgrsub2  42796  mpaaeu  42811  flcidc  42835  dflim5  42995  naddwordnexlem1  43064  rtrclexlem  43283  cnvrcl0  43292  brcoffn  43697  clsk1indlem3  43710  clsneif1o  43771  clsneicnv  43772  clsneikex  43773  clsneinex  43774  neicvgmex  43784  neicvgel1  43786  suprleubrd  43833  suprlubrd  43835  imo72b2  43839  dvconstbi  44008  bcc0  44014  binomcxplemnotnn0  44030  nnfoctb  44648  infleinflem1  44985  fprodcnlem  45220  sumnnodd  45251  icccncfext  45508  itgsin0pilem1  45571  stoweidlem32  45653  stoweidlem35  45656  stoweidlem36  45657  stoweidlem37  45658  stoweidlem43  45664  stoweidlem50  45671  wallispilem5  45690  stirlinglem2  45696  stirlinglem3  45697  stirlinglem4  45698  stirlinglem8  45702  stirlinglem11  45705  stirlinglem12  45706  stirlinglem14  45708  stirlinglem15  45709  fourierdlem11  45739  fourierdlem20  45748  fourierdlem21  45749  fourierdlem41  45769  fourierdlem42  45770  fourierdlem48  45775  fourierdlem49  45776  fourierdlem64  45791  fourierdlem71  45798  fourierdlem79  45806  fourierdlem90  45817  fourierdlem91  45818  fourierswlem  45851  etransclem17  45872  etransclem38  45893  saluni  45946  meaiininclem  46107  issmflelem  46365  issmfgtlem  46376  issmfgelem  46390  smflimsuplem4  46444  f1cof1blem  46689  sprval  47051  prprval  47086  bgoldbtbndlem2  47378  bgoldbtbndlem3  47379  bgoldbtbnd  47381  isubgrvtxuhgr  47431  isuspgrim  47454  grimcnv  47458  gricushgr  47465  uhgrimisgrgric  47478  grlictr  47505  isclintop  47584  clintopcllaw  47588  nzrneg1ne0  47607  lidldomn1  47608  zlidlring  47611  uzlidlring  47612  2zrngnmlid  47632  cznrng  47638  coe1id  47767  blenre  47962  blennn  47963  2arymaptf  48040  itcoval1  48051  itcovalendof  48057  ehl2eudisval0  48113  eenglngeehlnmlem2  48126  itsclc0yqsol  48152  inlinecirc02plem  48174  ipolub  48314  ipoglb  48317  setrec2mpt  48443