Theorem mpdan 684

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  mpidan  686  mpan2  688  biadanid  820  mpjaodan  956  mpjao3dan  1430  mpd3an3  1461  elabd2  3611  eueq2  3655  csbiegf  3876  difsnb  4751  reusv3i  5342  frpoinsg  6269  fimadmfo  6735  fimadmfoALT  6737  fvtresfn  6917  fvmpt3  6919  ffvelcdmd  7002  fnressn  7070  fsnex  7195  f1oiso2  7263  riota5f  7303  suceloni  7703  onsucuni  7720  frrlem10  8160  seqomlem2  8331  oaordi  8427  nnaordi  8499  qsdisj  8633  dom2lem  8832  canth2g  8975  limenpsi  8996  nnfi  9011  php4  9057  onfin  9074  sucxpdom  9099  xpfiOLD  9162  dmfi  9174  pwfilemOLD  9190  pwfiOLD  9191  fiin  9258  supiso  9311  ordiso2  9351  wdom2d  9416  infeq5  9473  cantnfp1lem3  9516  cantnflem1d  9524  rankwflemb  9629  onenon  9785  cardonle  9793  sdomsdomcardi  9807  acni  9881  cardaleph  9925  djuen  10005  djuinf  10024  infdju1  10025  nnadju  10033  pwsdompw  10040  infdif  10045  cfval  10083  fin34  10226  fin1a2lem1  10236  fin1a2  10251  ttukeylem6  10350  sdomsdomcard  10396  canth3  10397  fpwwe2  10479  canthwelem  10486  gchdju1  10492  pwfseqlem4  10498  gchdjuidm  10504  gchxpidm  10505  tskwe2  10609  rankcf  10613  tskuni  10619  gruxp  10643  dmrecnq  10804  lterpq  10806  archnq  10816  reclem3pr  10885  reclem4pr  10886  0idsr  10933  lep1  11896  ledivp1  11957  negfi  12004  supaddc  12022  supmul1  12024  suprzcl  12480  uz11  12687  zmin  12764  zbtwnre  12766  rpnnen1lem4  12800  rpnnen1lem5  12801  xnegid  13052  supxrre  13141  infxrre  13150  eluzfz2  13344  fzsuc  13383  fzsuc2  13394  fzp1disj  13395  fzneuz  13417  nn0p1elfzo  13510  fllep1  13601  fraclt1  13602  fracle1  13603  fracge0  13604  flhalf  13630  ceige  13644  ceim1l  13647  fldiv  13660  modval  13671  suppssfz  13794  seqeq1  13804  expubnd  13975  iexpcyc  14003  binom2sub1  14016  faclbnd4lem3  14089  pfxid  14476  pfxccatpfx2  14529  swrdccat3blem  14531  cshw0  14586  cshwn  14589  cshimadifsn  14621  cshimadifsn0  14622  pfx2  14739  trclexlem  14784  shftfval  14860  shftcan1  14873  reval  14896  cjmulrcl  14934  addcj  14938  absval  15028  absneg  15068  abscj  15070  sqabsadd  15073  sqabssub  15074  leabs  15090  sqreulem  15150  lo1res  15347  o1of2  15401  o1rlimmul  15407  flo1  15645  trirecip  15654  efcan  15884  efi4p  15925  resin4p  15926  recos4p  15927  sincossq  15964  ruclem10  16027  iddvds  16058  1dvds  16059  2ebits  16233  lcmftp  16418  coprmgcdb  16431  1idssfct  16462  exprmfct  16486  eulerthlem2  16560  odzphi  16574  pcprendvds  16618  pcmpt  16670  oddprmdvds  16681  vdwlem8  16766  0ram2  16799  prmgaplem7  16835  setsn0fun  16951  setsexstruct2  16953  pwsvscaval  17283  2initoinv  17802  initoeu1  17803  initoeu2lem1  17806  initoeu2  17808  2termoinv  17809  termoeu1  17810  homarel  17828  joinfval  18168  meetfval  18182  latjcom  18242  latmcom  18258  0subm  18533  sgrp2nmndlem5  18644  grprcan  18689  isgrpid2  18692  grpinvid  18712  mulgnn0z  18806  0subg  18856  qus0  18890  ghmker  18936  symgbasmap  19060  symginv  19086  pmtrfrn  19142  odmulg2  19238  slwpgp  19294  pj1eq  19381  efgtf  19403  frgpinv  19445  frgpup2  19457  cnaddablx  19544  cnaddabl  19545  zaddablx  19548  dprdfadd  19698  dpjidcl  19736  dpjlid  19739  pgpfac1lem3  19755  srgen1zr  19841  1unit  19975  unitgrpid  19986  1rinv  19996  irredn0  20020  irredneg  20027  isdrng2  20083  rnrhmsubrg  20138  abv0  20174  abv1z  20175  abvneg  20177  lmodfopne  20244  lsssn0  20292  lspsn0  20353  lsp0  20354  lmhmvsca  20390  lmhmrnlss  20395  lmhmkerlss  20396  lsppratlem5  20496  rsp1  20578  ringen1zr  20631  cnfldneg  20707  zringcyg  20774  chrid  20814  chrrhm  20818  ip0r  20925  ocvlss  20960  ocv1  20967  rlmassa  21158  psrbagfsupp  21206  snifpsrbag  21208  psrbaglefi  21218  psrvscaval  21244  psrdi  21258  psrdir  21259  mplvscaval  21303  mhpmpl  21417  mhpdeg  21418  mhppwdeg  21423  coe1sclmulfv  21537  ply1idvr1  21547  evl1var  21585  mamuvs1  21635  mamuvs2  21636  matecl  21657  matvscacell  21668  mat0scmat  21770  submaval0  21812  mdetrsca  21835  maduval  21870  minmar1val0  21879  pmatcollpw3fi1lem2  22019  chcoeffeqlem  22117  cayleyhamilton0  22121  cayleyhamiltonALT  22123  toponsspwpw  22154  cctop  22239  cldval  22257  ntrfval  22258  clsfval  22259  cmclsopn  22296  opncldf3  22320  neifval  22333  lpfval  22372  cnrmnrm  22595  dis2ndc  22694  islocfin  22751  tx1cn  22843  idqtop  22940  kqtopon  22961  kqid  22962  kqcld  22969  hmphen2  23033  filssufil  23146  ufileu  23153  alexsublem  23278  efmndtmd  23335  symgtgp  23340  ustuqtop4  23479  cstucnd  23519  metustexhalf  23795  nm0  23868  rlmnlm  23935  nmolb  23964  metdseq0  24100  pi1xfrval  24300  clmvneg1  24345  clmvsubval  24355  ipcau2  24481  tcphcphlem1  24482  tcphcphlem2  24483  cmetcaulem  24535  ovolicc2lem3  24766  ovolicc2lem4  24767  mbfmulc2lem  24894  i1fpos  24954  mbfi1fseqlem3  24965  itg2ge0  24983  bddiblnc  25089  dvres2  25159  dvaddbr  25185  dvmulbr  25186  dvcobr  25193  dvfsumlem4  25276  ftc1a  25284  ftc1lem6  25288  uc1pmon1p  25399  ig1pval2  25421  dgradd2  25512  dgrcolem2  25518  plydivlem4  25539  plydiveu  25541  elqaalem3  25564  qaa  25566  ulmdvlem1  25642  abelthlem6  25678  abelthlem7  25680  eflogeq  25840  jensenlem2  26220  harmonicbnd4  26243  sgmnncl  26379  dchrptlem2  26496  1lgs  26571  lgs1  26572  2sqcoprm  26666  addsqnreup  26674  dchrisumlem2  26721  dchrisum0lem2a  26748  selberg2lem  26781  pntrsumo1  26796  pntrsumbnd  26797  pntpbnd1  26817  pntlemr  26833  pntlemj  26834  padicabvf  26862  bdayval  26879  noextendgt  26901  incistruhgr  27585  subgrprop3  27779  subgruhgredgd  27787  usgrexi  27944  cusgrexi  27946  cusgrsizeinds  27955  vtxdgfusgrf  28000  1hevtxdg1  28009  1egrvtxdg1  28012  ewlkprop  28106  wlklenvm1  28125  wlkl1loop  28141  wlkp1lem4  28180  2pthnloop  28235  upgrclwlkcompim  28285  crctcshwlkn0lem4  28314  crctcshwlkn0lem5  28315  crctcshwlkn0lem6  28316  crctcshwlkn0lem7  28317  crctcshlem4  28321  wspthnonp  28360  wlkswwlksf1o  28380  wwlksnwwlksnon  28416  umgr2wlkon  28451  wwlks2onv  28454  elwwlks2ons3im  28455  elwspths2spth  28468  umgrclwwlkge2  28491  clwlkclwwlkf1lem3  28506  erclwwlkref  28520  clwwlknp  28537  wwlksext2clwwlk  28557  wwlksubclwwlk  28558  0pthon1  28628  1wlkdlem4  28640  1pthd  28643  3spthd  28676  eupth2eucrct  28717  eucrctshift  28743  eucrct2eupth  28745  frgrncvvdeqlem8  28806  frgr2wwlkeqm  28831  isgrpoi  28996  grpoinvfval  29020  grpodivfval  29032  vcz  29073  cnaddabloOLD  29079  nvz0  29166  sspz  29233  lno0  29254  nmobndi  29273  ipasslem2  29330  shunssi  29866  ococin  29906  ssjo  29945  pjocini  30196  nlfnval  30379  lncnopbd  30535  riesz3i  30560  cnlnadjlem7  30571  pjclem4  30697  pj3si  30705  hstoc  30720  hstnmoc  30721  hstoh  30730  hst0  30731  mdsl2i  30820  chirredlem3  30890  chirredlem4  30891  dmdbr5ati  30920  rexunirn  30976  fcnvgreu  31145  infxrge0glb  31223  omndmul2  31473  omndmul  31475  cycpmco2lem5  31532  cycpmco2lem6  31533  cycpmco2lem7  31534  isarchi3  31576  orng0le1  31653  nsgqusf1olem2  31738  kerlidl  31743  ssmxidllem  31780  fedgmullem1  31850  extdg1id  31878  zartopn  31965  zarcmplem  31971  esumcvg  32194  esumcvgre  32199  sigaval  32219  unelldsys  32266  fiunelros  32282  measval  32306  pmeasmono  32431  probfinmeasb  32535  ballotlemfc0  32599  ballotlemfcc  32600  ballotlemsi  32621  ballotlemfrci  32634  sgnneg  32647  signlem0  32706  breprexp  32753  bnj1006  33079  bnj1110  33101  bnj1253  33136  bnj1280  33139  bnj1463  33174  bnj1312  33177  erdszelem7  33298  erdszelem8  33299  cvmliftlem10  33395  cvmliftlem13  33397  cvmlift2lem9  33412  cvmlift3lem6  33425  cvmlift3lem7  33426  cvmlift3lem9  33428  satfv1lem  33463  dfrdg2  33902  nosupbnd2lem1  33992  noinfbnd2lem1  34007  noetainflem4  34017  oldval  34112  cldregopn  34594  tailfval  34635  filnetlem3  34643  filnetlem4  34644  ontopbas  34691  bj-elid4  35411  bj-imdiridlem  35428  f1omptsnlem  35579  icoreunrn  35602  relowlpssretop  35607  fvineqsnf1  35653  wl-sbal2  35791  unccur  35832  poimirlem1  35850  poimirlem2  35851  poimirlem4  35853  poimirlem6  35855  poimirlem7  35856  poimirlem11  35860  poimirlem12  35861  poimirlem17  35866  poimirlem20  35869  poimirlem22  35871  poimirlem23  35872  poimirlem28  35877  poimir  35882  ismblfin  35890  cnambfre  35897  ftc1cnnc  35921  dvasin  35933  ismtyres  36038  heiborlem8  36048  ghomidOLD  36119  rngosn6  36156  rngonegmn1l  36171  rngonegmn1r  36172  rngoneglmul  36173  rngonegrmul  36174  idlnegcl  36252  0idl  36255  0rngo  36257  smprngopr  36282  cossex  36653  qsdisjALTV  36849  cnvepresdmqss  36886  mpets2  37075  lkrval  37322  ldualvaddval  37365  ldualvsval  37372  opoc1  37436  pmap0  38000  pmap1N  38002  pexmidALTN  38213  cdleme31fv  38625  cdlemg27b  38931  erngdvlem4  39226  erng0g  39229  erngdvlem4-rN  39234  dvalveclem  39260  dvh0g  39346  dih0cnv  39518  dih1rn  39522  dih1cnv  39523  doch0  39593  doch1  39594  lcfl7lem  39734  mapdheq  39963  hdmap1eq  40036  hdmapval2lem  40066  hgmapvvlem3  40160  lcmineqlem13  40270  aks4d1p9  40317  sticksstones1  40326  sticksstones6  40331  sticksstones7  40332  sticksstones11  40336  sticksstones12a  40337  sticksstones12  40338  sticksstones22  40348  frlmsnic  40479  fsuppssind  40498  renegid  40572  sn-0ne2  40605  remul01  40606  remulinvcom  40630  sn-0tie0  40637  sn-inelr  40651  mzpval  40770  mzpindd  40784  pellex  40873  2nn0ind  40984  jm2.26lem3  41040  pw2f1o2val  41078  wepwsolem  41084  fnwe2lem3  41094  lnmfg  41124  dgrsub2  41177  mpaaeu  41192  flcidc  41216  rtrclexlem  41458  cnvrcl0  41467  brcoffn  41874  clsk1indlem3  41887  clsneif1o  41948  clsneicnv  41949  clsneikex  41950  clsneinex  41951  neicvgmex  41961  neicvgel1  41963  suprleubrd  42011  suprlubrd  42013  imo72b2  42017  dvconstbi  42186  bcc0  42192  binomcxplemnotnn0  42208  nnfoctb  42829  infleinflem1  43158  fprodcnlem  43390  sumnnodd  43421  icccncfext  43678  itgsin0pilem1  43741  stoweidlem32  43823  stoweidlem35  43826  stoweidlem36  43827  stoweidlem37  43828  stoweidlem43  43834  stoweidlem50  43841  wallispilem5  43860  stirlinglem2  43866  stirlinglem3  43867  stirlinglem4  43868  stirlinglem8  43872  stirlinglem11  43875  stirlinglem12  43876  stirlinglem14  43878  stirlinglem15  43879  fourierdlem11  43909  fourierdlem20  43918  fourierdlem21  43919  fourierdlem41  43939  fourierdlem42  43940  fourierdlem48  43945  fourierdlem49  43946  fourierdlem64  43961  fourierdlem71  43968  fourierdlem79  43976  fourierdlem90  43987  fourierdlem91  43988  fourierswlem  44021  etransclem17  44042  etransclem38  44063  saluni  44115  meaiininclem  44275  issmflelem  44533  issmfgtlem  44544  issmfgelem  44558  smflimsuplem4  44612  f1cof1blem  44833  sprval  45196  prprval  45231  bgoldbtbndlem2  45523  bgoldbtbndlem3  45524  bgoldbtbnd  45526  isomushgr  45543  isomuspgrlem1  45544  isclintop  45666  clintopcllaw  45670  nzrneg1ne0  45692  c0snmgmhm  45737  zrrnghm  45740  lidldomn1  45744  zlidlring  45751  uzlidlring  45752  2zrngnmlid  45772  cznrng  45778  zrinitorngc  45823  zrtermorngc  45824  zrtermoringc  45893  coe1id  45990  blenre  46185  blennn  46186  2arymaptf  46263  itcoval1  46274  itcovalendof  46280  ehl2eudisval0  46336  eenglngeehlnmlem2  46349  itsclc0yqsol  46375  inlinecirc02plem  46397  ipolub  46539  ipoglb  46542