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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  mpidan  688  mpan2  690  biadanid  822  mpjaodan  957  mpjao3dan  1429  mpd3an3  1459  elabd2  3656  eueq2  3703  csbiegf  3923  difsnb  4805  reusv3i  5398  frpoinsg  6343  fimadmfo  6814  fimadmfoALT  6816  fvtresfn  7001  fvmpt3  7003  ffvelcdmd  7089  fnressn  7161  fsnex  7286  f1oiso2  7354  riota5f  7399  onsuc  7808  onsucuni  7825  frrlem10  8294  seqomlem2  8465  oaordi  8560  nnaordi  8632  qsdisj  8804  dom2lem  9004  canth2g  9147  limenpsi  9168  nnfi  9183  php4  9229  onfin  9246  sucxpdom  9271  xpfiOLD  9334  dmfi  9346  pwfilemOLD  9362  pwfiOLD  9363  fiin  9437  supiso  9490  ordiso2  9530  wdom2d  9595  infeq5  9652  cantnfp1lem3  9695  cantnflem1d  9703  rankwflemb  9808  onenon  9964  cardonle  9972  sdomsdomcardi  9986  acni  10060  cardaleph  10104  djuen  10184  djuinf  10203  infdju1  10204  nnadju  10212  pwsdompw  10219  infdif  10224  cfval  10262  fin34  10405  fin1a2lem1  10415  fin1a2  10430  ttukeylem6  10529  sdomsdomcard  10575  canth3  10576  fpwwe2  10658  canthwelem  10665  gchdju1  10671  pwfseqlem4  10677  gchdjuidm  10683  gchxpidm  10684  tskwe2  10788  rankcf  10792  tskuni  10798  gruxp  10822  dmrecnq  10983  lterpq  10985  archnq  10995  reclem3pr  11064  reclem4pr  11065  0idsr  11112  lep1  12077  ledivp1  12138  negfi  12185  supaddc  12203  supmul1  12205  suprzcl  12664  uz11  12869  zmin  12950  zbtwnre  12952  rpnnen1lem4  12986  rpnnen1lem5  12987  xnegid  13241  supxrre  13330  infxrre  13339  eluzfz2  13533  fzsuc  13572  fzsuc2  13583  fzp1disj  13584  fzneuz  13606  nn0p1elfzo  13699  fllep1  13790  fraclt1  13791  fracle1  13792  fracge0  13793  flhalf  13819  ceige  13833  ceim1l  13836  fldiv  13849  modval  13860  suppssfz  13983  seqeq1  13993  expubnd  14165  iexpcyc  14194  binom2sub1  14207  faclbnd4lem3  14278  pfxid  14658  pfxccatpfx2  14711  swrdccat3blem  14713  cshw0  14768  cshwn  14771  cshimadifsn  14804  cshimadifsn0  14805  pfx2  14922  trclexlem  14965  shftfval  15041  shftcan1  15054  reval  15077  cjmulrcl  15115  addcj  15119  absval  15209  absneg  15248  abscj  15250  sqabsadd  15253  sqabssub  15254  leabs  15270  sqreulem  15330  lo1res  15527  o1of2  15581  o1rlimmul  15587  flo1  15824  trirecip  15833  efcan  16064  efi4p  16105  resin4p  16106  recos4p  16107  sincossq  16144  ruclem10  16207  iddvds  16238  1dvds  16239  2ebits  16413  lcmftp  16598  coprmgcdb  16611  1idssfct  16642  exprmfct  16666  eulerthlem2  16742  odzphi  16756  pcprendvds  16800  pcmpt  16852  oddprmdvds  16863  vdwlem8  16948  0ram2  16981  prmgaplem7  17017  setsn0fun  17133  setsexstruct2  17135  pwsvscaval  17468  2initoinv  17990  initoeu1  17991  initoeu2lem1  17994  initoeu2  17996  2termoinv  17997  termoeu1  17998  homarel  18016  joinfval  18356  meetfval  18370  latjcom  18430  latmcom  18446  0subm  18760  sgrp2nmndlem5  18872  grprcan  18921  isgrpid2  18924  grpinvid  18947  mulgnn0z  19047  0subgOLD  19098  qus0  19135  eqg0subg  19142  ghmker  19187  symgbasmap  19322  symginv  19348  pmtrfrn  19404  odmulg2  19501  slwpgp  19559  pj1eq  19646  efgtf  19668  frgpinv  19710  frgpup2  19722  cnaddablx  19814  cnaddabl  19815  zaddablx  19818  imasabl  19822  dprdfadd  19968  dpjidcl  20006  dpjlid  20009  pgpfac1lem3  20025  srgen1zr  20147  1unit  20302  unitgrpid  20313  1rinv  20323  irredn0  20351  irredneg  20358  c0snmgmhm  20390  rngisomring1  20396  zrrnghm  20462  rnrhmsubrg  20533  zrinitorngc  20564  zrtermorngc  20565  zrtermoringc  20597  isdrng2  20627  ringen1zr  20655  abv0  20700  abv1z  20701  abvneg  20703  lmodfopne  20772  lsssn0  20821  lspsn0  20881  lsp0  20882  lmhmvsca  20919  lmhmrnlss  20924  lmhmkerlss  20925  lsppratlem5  21028  rsp1  21122  ring2idlqus  21188  rngqiprngfulem4  21193  rngqiprngfu  21196  cnfldneg  21310  zringcyg  21382  chrid  21442  chrrhm  21448  ip0r  21556  ocvlss  21591  ocv1  21598  rlmassa  21791  psrbagfsupp  21840  snifpsrbag  21842  psrbaglefi  21852  psrvscaval  21880  psrdi  21895  psrdir  21896  mplvscaval  21945  mhpmpl  22055  mhpdeg  22056  mhppwdeg  22061  psdmul  22077  coe1sclmulfv  22189  ply1idvr1  22201  evl1var  22242  mamuvs1  22292  mamuvs2  22293  matecl  22314  matvscacell  22325  mat0scmat  22427  submaval0  22469  mdetrsca  22492  maduval  22527  minmar1val0  22536  pmatcollpw3fi1lem2  22676  chcoeffeqlem  22774  cayleyhamilton0  22778  cayleyhamiltonALT  22780  toponsspwpw  22811  cctop  22896  cldval  22914  ntrfval  22915  clsfval  22916  cmclsopn  22953  opncldf3  22977  neifval  22990  lpfval  23029  cnrmnrm  23252  dis2ndc  23351  islocfin  23408  tx1cn  23500  idqtop  23597  kqtopon  23618  kqid  23619  kqcld  23626  hmphen2  23690  filssufil  23803  ufileu  23810  alexsublem  23935  efmndtmd  23992  symgtgp  23997  ustuqtop4  24136  cstucnd  24176  metustexhalf  24452  nm0  24525  rlmnlm  24592  nmolb  24621  metdseq0  24757  pi1xfrval  24968  clmvneg1  25013  clmvsubval  25023  ipcau2  25149  tcphcphlem1  25150  tcphcphlem2  25151  cmetcaulem  25203  ovolicc2lem3  25435  ovolicc2lem4  25436  mbfmulc2lem  25563  i1fpos  25623  mbfi1fseqlem3  25634  itg2ge0  25652  bddiblnc  25758  dvres2  25828  dvaddbr  25855  dvmulbr  25856  dvmulbrOLD  25857  dvcobr  25864  dvcobrOLD  25865  dvfsumlem4  25951  ftc1a  25959  ftc1lem6  25963  uc1pmon1p  26074  ig1pval2  26098  dgradd2  26190  dgrcolem2  26196  plydivlem4  26218  plydiveu  26220  elqaalem3  26243  qaa  26245  ulmdvlem1  26323  abelthlem6  26360  abelthlem7  26362  eflogeq  26523  jensenlem2  26907  harmonicbnd4  26930  sgmnncl  27066  dchrptlem2  27185  1lgs  27260  lgs1  27261  2sqcoprm  27355  addsqnreup  27363  dchrisumlem2  27410  dchrisum0lem2a  27437  selberg2lem  27470  pntrsumo1  27485  pntrsumbnd  27486  pntpbnd1  27506  pntlemr  27522  pntlemj  27523  padicabvf  27551  bdayval  27568  noextendgt  27590  nosupbnd2lem1  27635  noinfbnd2lem1  27650  noetainflem4  27660  oldval  27768  divsmul  28106  divscl  28108  seqsp1  28171  remulscllem1  28215  incistruhgr  28879  subgrprop3  29076  subgruhgredgd  29084  usgrexi  29241  cusgrexi  29243  cusgrsizeinds  29253  vtxdgfusgrf  29298  1hevtxdg1  29307  1egrvtxdg1  29310  ewlkprop  29404  wlklenvm1  29423  wlkl1loop  29439  wlkp1lem4  29477  2pthnloop  29532  upgrclwlkcompim  29582  crctcshwlkn0lem4  29611  crctcshwlkn0lem5  29612  crctcshwlkn0lem6  29613  crctcshwlkn0lem7  29614  crctcshlem4  29618  wspthnonp  29657  wlkswwlksf1o  29677  wwlksnwwlksnon  29713  umgr2wlkon  29748  wwlks2onv  29751  elwwlks2ons3im  29752  elwspths2spth  29765  umgrclwwlkge2  29788  clwlkclwwlkf1lem3  29803  erclwwlkref  29817  clwwlknp  29834  wwlksext2clwwlk  29854  wwlksubclwwlk  29855  0pthon1  29925  1wlkdlem4  29937  1pthd  29940  3spthd  29973  eupth2eucrct  30014  eucrctshift  30040  eucrct2eupth  30042  frgrncvvdeqlem8  30103  frgr2wwlkeqm  30128  isgrpoi  30295  grpoinvfval  30319  grpodivfval  30331  vcz  30372  cnaddabloOLD  30378  nvz0  30465  sspz  30532  lno0  30553  nmobndi  30572  ipasslem2  30629  shunssi  31165  ococin  31205  ssjo  31244  pjocini  31495  nlfnval  31678  lncnopbd  31834  riesz3i  31859  cnlnadjlem7  31870  pjclem4  31996  pj3si  32004  hstoc  32019  hstnmoc  32020  hstoh  32029  hst0  32030  mdsl2i  32119  chirredlem3  32189  chirredlem4  32190  dmdbr5ati  32219  rexunirn  32276  fcnvgreu  32442  infxrge0glb  32519  omndmul2  32770  omndmul  32772  cycpmco2lem5  32829  cycpmco2lem6  32830  cycpmco2lem7  32831  isarchi3  32873  orng0le1  32967  nsgqusf1olem2  33064  kerlidl  33071  ssmxidllem  33122  ressply1sub  33181  fedgmullem1  33259  extdg1id  33287  zartopn  33412  zarcmplem  33418  esumcvg  33641  esumcvgre  33646  sigaval  33666  unelldsys  33713  fiunelros  33729  measval  33753  pmeasmono  33880  probfinmeasb  33984  ballotlemfc0  34048  ballotlemfcc  34049  ballotlemsi  34070  ballotlemfrci  34083  sgnneg  34096  signlem0  34155  breprexp  34201  bnj1006  34527  bnj1110  34549  bnj1253  34584  bnj1280  34587  bnj1463  34622  bnj1312  34625  erdszelem7  34743  erdszelem8  34744  cvmliftlem10  34840  cvmliftlem13  34842  cvmlift2lem9  34857  cvmlift3lem6  34870  cvmlift3lem7  34871  cvmlift3lem9  34873  satfv1lem  34908  dfrdg2  35327  cldregopn  35751  tailfval  35792  filnetlem3  35800  filnetlem4  35801  ontopbas  35848  bj-elid4  36583  bj-imdiridlem  36600  f1omptsnlem  36751  icoreunrn  36774  relowlpssretop  36779  fvineqsnf1  36825  wl-sbal2  36966  unccur  37011  poimirlem1  37029  poimirlem2  37030  poimirlem4  37032  poimirlem6  37034  poimirlem7  37035  poimirlem11  37039  poimirlem12  37040  poimirlem17  37045  poimirlem20  37048  poimirlem22  37050  poimirlem23  37051  poimirlem28  37056  poimir  37061  ismblfin  37069  cnambfre  37076  ftc1cnnc  37100  dvasin  37112  ismtyres  37216  heiborlem8  37226  ghomidOLD  37297  rngosn6  37334  rngonegmn1l  37349  rngonegmn1r  37350  rngoneglmul  37351  rngonegrmul  37352  idlnegcl  37430  0idl  37433  0rngo  37435  smprngopr  37460  cossex  37828  qsdisjALTV  38024  cnvepresdmqss  38061  mpets2  38250  lkrval  38497  ldualvaddval  38540  ldualvsval  38547  opoc1  38611  pmap0  39175  pmap1N  39177  pexmidALTN  39388  cdleme31fv  39800  cdlemg27b  40106  erngdvlem4  40401  erng0g  40404  erngdvlem4-rN  40409  dvalveclem  40435  dvh0g  40521  dih0cnv  40693  dih1rn  40697  dih1cnv  40698  doch0  40768  doch1  40769  lcfl7lem  40909  mapdheq  41138  hdmap1eq  41211  hdmapval2lem  41241  hgmapvvlem3  41335  lcmineqlem13  41449  aks4d1p9  41496  primrootsunit1  41504  aks6d1c1p1  41511  aks6d1c1p6  41518  aks6d1c1p8  41519  sticksstones1  41550  sticksstones6  41555  sticksstones7  41556  sticksstones11  41560  sticksstones12a  41561  sticksstones12  41562  sticksstones22  41572  frlmsnic  41692  fsuppssind  41748  renegid  41850  sn-0ne2  41883  remul01  41884  remulinvcom  41909  sn-0tie0  41916  renegmulnnass  41930  sn-inelr  41942  mzpval  42074  mzpindd  42088  pellex  42177  2nn0ind  42288  jm2.26lem3  42344  pw2f1o2val  42382  wepwsolem  42388  fnwe2lem3  42398  lnmfg  42428  dgrsub2  42481  mpaaeu  42496  flcidc  42520  dflim5  42681  naddwordnexlem1  42750  rtrclexlem  42969  cnvrcl0  42978  brcoffn  43383  clsk1indlem3  43396  clsneif1o  43457  clsneicnv  43458  clsneikex  43459  clsneinex  43460  neicvgmex  43470  neicvgel1  43472  suprleubrd  43519  suprlubrd  43521  imo72b2  43525  dvconstbi  43694  bcc0  43700  binomcxplemnotnn0  43716  nnfoctb  44334  infleinflem1  44675  fprodcnlem  44910  sumnnodd  44941  icccncfext  45198  itgsin0pilem1  45261  stoweidlem32  45343  stoweidlem35  45346  stoweidlem36  45347  stoweidlem37  45348  stoweidlem43  45354  stoweidlem50  45361  wallispilem5  45380  stirlinglem2  45386  stirlinglem3  45387  stirlinglem4  45388  stirlinglem8  45392  stirlinglem11  45395  stirlinglem12  45396  stirlinglem14  45398  stirlinglem15  45399  fourierdlem11  45429  fourierdlem20  45438  fourierdlem21  45439  fourierdlem41  45459  fourierdlem42  45460  fourierdlem48  45465  fourierdlem49  45466  fourierdlem64  45481  fourierdlem71  45488  fourierdlem79  45496  fourierdlem90  45507  fourierdlem91  45508  fourierswlem  45541  etransclem17  45562  etransclem38  45583  saluni  45636  meaiininclem  45797  issmflelem  46055  issmfgtlem  46066  issmfgelem  46080  smflimsuplem4  46134  f1cof1blem  46379  sprval  46742  prprval  46777  bgoldbtbndlem2  47069  bgoldbtbndlem3  47070  bgoldbtbnd  47072  isuspgrim  47096  grimcnv  47100  gricushgr  47106  isclintop  47192  clintopcllaw  47196  nzrneg1ne0  47215  lidldomn1  47216  zlidlring  47219  uzlidlring  47220  2zrngnmlid  47240  cznrng  47246  coe1id  47375  blenre  47570  blennn  47571  2arymaptf  47648  itcoval1  47659  itcovalendof  47665  ehl2eudisval0  47721  eenglngeehlnmlem2  47734  itsclc0yqsol  47760  inlinecirc02plem  47782  ipolub  47922  ipoglb  47925  setrec2mpt  48051