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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  mpidan  701  mpan2  703  mpjaodan  823  mpd3an3  1417  eueq2  3347  csbiegf  3523  difsnb  4278  reusv3i  4801  fvtresfn  6193  fvmpt3  6195  ffvelrnd  6268  fnressn  6330  fsnex  6438  f1oiso2  6502  riota5f  6535  onsucuni  6920  wfrlem5  7306  seqomlem2  7433  oaordi  7513  nnaordi  7585  qsdisj  7711  dom2lem  7881  canth2g  7999  limenpsi  8020  php4  8032  onfin  8036  sucxpdom  8054  xpfi  8116  dmfi  8129  pwfilem  8143  pwfi  8144  fiin  8211  supiso  8264  ordiso2  8303  wdom2d  8368  infeq5  8417  cantnfp1lem3  8460  cantnflem1d  8468  rankwflemb  8539  onenon  8658  cardonle  8666  sdomsdomcardi  8680  acni  8751  cardaleph  8795  cdaen  8878  cdainf  8897  infcda1  8898  pwsdompw  8909  infdif  8914  cfval  8952  fin34  9095  fin1a2lem1  9105  fin1a2  9120  ttukeylem6  9219  sdomsdomcard  9261  canth3  9262  fpwwe2  9344  canthwelem  9351  gchcda1  9357  pwfseqlem4  9363  gchcdaidm  9369  gchxpidm  9370  tskwe2  9474  rankcf  9478  tskuni  9484  gruxp  9508  dmrecnq  9669  lterpq  9671  archnq  9681  reclem3pr  9750  reclem4pr  9751  0idsr  9797  lep1  10741  ledivp1  10804  negfi  10850  supaddc  10867  supmul1  10869  suprzcl  11333  uz11  11586  zmin  11660  zbtwnre  11662  rpnnen1lem4  11693  rpnnen1lem5  11694  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  xnegid  11943  xrsupss  12011  xrinfmss  12012  supxrre  12029  infxrre  12038  eluzfz2  12220  fzsuc  12258  fzsuc2  12268  fzp1disj  12269  fzneuz  12290  nn0p1elfzo  12378  fllep1  12464  fraclt1  12465  fracle1  12466  fracge0  12467  flhalf  12493  ceige  12506  ceim1l  12508  fldiv  12521  modval  12532  suppssfz  12656  seqeq1  12666  expubnd  12783  iexpcyc  12831  binom2sub1  12844  faclbnd4lem3  12944  swrdid  13280  swrdccat3blem  13346  cshwn  13394  cshimadifsn  13426  cshimadifsn0  13427  trclexlem  13581  shftfval  13658  shftcan1  13671  reval  13694  cjmulrcl  13732  addcj  13736  absval  13826  absneg  13865  abscj  13867  sqabsadd  13870  sqabssub  13871  leabs  13887  sqreulem  13947  lo1res  14138  o1of2  14191  o1rlimmul  14197  flo1  14425  trirecip  14434  efcan  14665  efi4p  14706  resin4p  14707  recos4p  14708  sincossq  14745  ruclem10  14807  iddvds  14833  1dvds  14834  2ebits  15007  lcmftp  15187  coprmgcdb  15200  1idssfct  15231  exprmfct  15254  eulerthlem2  15325  odzphi  15339  pcprendvds  15383  pcmpt  15434  vdwlem8  15530  0ram2  15563  prmgaplem7  15599  pwsvscaval  15978  issect2  16237  2initoinv  16483  initoeu1  16484  initoeu2lem1  16487  initoeu2  16489  2termoinv  16490  termoeu1  16491  homarel  16509  joinfval  16824  meetfval  16838  latjcom  16882  latmcom  16898  sgrp2nmndlem5  17239  grprcan  17278  isgrpid2  17281  grpinvid  17299  mulgnn0z  17390  0subg  17442  qus0  17475  ghmker  17509  symginv  17645  pmtrfrn  17701  odmulg2  17795  slwpgp  17851  pj1eq  17936  efgtf  17958  frgpinv  18000  frgpup2  18012  mulgnn0di  18054  cnaddablx  18094  cnaddabl  18095  zaddablx  18098  dprdfadd  18242  dpjidcl  18280  dpjlid  18283  pgpfac1lem3  18299  srgen1zr  18353  ringlz  18410  ringrz  18411  1unit  18481  unitgrpid  18492  1rinv  18502  irredn0  18526  irredneg  18533  isdrng2  18580  abv0  18654  abv1z  18655  abvneg  18657  lmodfopne  18724  lsssn0  18769  lspsn0  18829  lsp0  18830  lmhmvsca  18866  lmhmrnlss  18871  lmhmkerlss  18872  lsppratlem5  18972  rsp1  19045  ringen1zr  19098  rlmassa  19147  snifpsrbag  19187  psrvscaval  19213  psrdi  19227  psrdir  19228  mplsubglem  19255  mplvscaval  19269  coe1sclmulfv  19474  ply1idvr1  19484  evl1var  19521  cnfldneg  19591  zringcyg  19658  chrid  19694  chrrhm  19698  ip0r  19801  ocvlss  19835  ocv1  19842  mamuvs1  20030  mamuvs2  20031  matecl  20050  matvscacell  20061  mat0scmat  20163  submaval0  20205  mdetrsca  20228  maduval  20263  minmar1val0  20272  pmatcollpw3fi1lem2  20411  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  chcoeffeqlem  20509  cayleyhamilton0  20513  cayleyhamiltonALT  20515  cctop  20620  cldval  20637  ntrfval  20638  clsfval  20639  cmclsopn  20676  opncldf3  20700  neifval  20713  lpfval  20752  cnrmnrm  20975  islocfin  21130  tx1cn  21222  idqtop  21319  kqtopon  21340  kqid  21341  kqcld  21348  hmphen2  21412  filssufil  21526  ufileu  21533  alexsublem  21658  symgtgp  21715  ustuqtop4  21858  cstucnd  21898  metustexhalf  22171  nm0  22243  rlmnlm  22302  nmolb  22331  metdseq0  22465  pi1xfrval  22662  clmvneg1  22707  clmvsubval  22717  ipcau2  22841  tchcphlem1  22842  tchcphlem2  22843  cmetcaulem  22894  ovolicc2lem3  23094  ovolicc2lem4  23095  mbfmulc2lem  23220  i1fpos  23279  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  itg2ge0  23308  dvres2  23482  dvaddbr  23507  dvmulbr  23508  dvcobr  23515  dvfsumlem4  23596  ftc1a  23604  ftc1lem6  23608  uc1pmon1p  23715  ig1pval2  23737  dgradd2  23828  dgrcolem2  23834  plydivlem4  23855  plydiveu  23857  elqaalem3  23880  qaa  23882  ulmdvlem1  23958  abelthlem6  23994  abelthlem7  23996  eflogeq  24152  jensenlem2  24514  harmonicbnd4  24537  sgmnncl  24673  dchrptlem2  24790  1lgs  24865  lgs1  24866  dchrisumlem2  24979  dchrisum0lem2a  25006  selberg2lem  25039  pntrsumo1  25054  pntrsumbnd  25055  pntpbnd1  25075  pntlemr  25091  pntlemj  25092  padicabvf  25120  istrkg3ld  25160  structiedg0val  25699  incistruhgr  25746  uhgredgiedgb  25799  uhgriedg0edg0  25801  cusgraexilem2  25996  cusgraexi  25997  cusgrasizeinds  26004  wwlksubclwwlk  26332  erclwwlkref  26341  erclwwlknref  26353  eupacl  26496  eupapf  26499  eupaseg  26500  frgrancvvdeqlemC  26566  frghash2spot  26590  isgrpoi  26736  grpoinvfval  26760  grpodivfval  26772  vcz  26814  cnaddabloOLD  26820  nvz0  26907  sspz  26974  lno0  26995  nmobndi  27014  ipasslem2  27071  shunssi  27611  ococin  27651  ssjo  27690  pjocini  27941  nlfnval  28124  lncnopbd  28280  riesz3i  28305  cnlnadjlem7  28316  pjclem4  28442  pj3si  28450  hstoc  28465  hstnmoc  28466  hstoh  28475  hst0  28476  mdsl2i  28565  chirredlem3  28635  chirredlem4  28636  dmdbr5ati  28665  rexunirn  28715  fcnvgreu  28855  infxrge0glb  28920  2sqcoprm  28978  omndmul2  29043  omndmul  29045  isarchi3  29072  orng0le1  29143  esumcvg  29475  esumcvgre  29480  sigaval  29500  unelldsys  29548  fiunelros  29564  measval  29588  pmeasmono  29713  eulerpartlemgvv  29765  probfinmeasb  29818  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemsi  29903  ballotlemfrci  29916  sgnneg  29929  signlem0  29990  bnj1006  30283  bnj1110  30304  bnj1253  30339  bnj1280  30342  bnj1463  30377  bnj1312  30380  erdszelem7  30433  erdszelem8  30434  cvmliftlem10  30530  cvmliftlem13  30532  cvmlift2lem9  30547  cvmlift3lem6  30560  cvmlift3lem7  30561  cvmlift3lem9  30563  dfrdg2  30945  dftrpred3g  30977  frrlem5  31028  bdayval  31045  cldregopn  31496  tailfval  31537  filnetlem3  31545  filnetlem4  31546  ontopbas  31597  bj-toponss  32241  f1omptsnlem  32359  icoreunrn  32383  relowlpssretop  32388  wl-sbal2  32526  unccur  32562  poimirlem1  32580  poimirlem2  32581  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem11  32590  poimirlem12  32591  poimirlem17  32596  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  poimirlem28  32607  poimir  32612  ismblfin  32620  cnambfre  32628  bddiblnc  32650  ftc1cnnc  32654  dvasin  32666  ismtyres  32777  heiborlem8  32787  ghomidOLD  32858  rngolz  32891  rngorz  32892  rngosn6  32895  rngonegmn1l  32910  rngonegmn1r  32911  rngoneglmul  32912  rngonegrmul  32913  idlnegcl  32991  0idl  32994  0rngo  32996  keridl  33001  smprngopr  33021  lshpne0  33291  lkrval  33393  ldualvaddval  33436  ldualvsval  33443  opoc1  33507  pmap0  34069  pmap1N  34071  pexmidALTN  34282  cdleme31fv  34696  cdlemg27b  35002  erngdvlem4  35297  erng0g  35300  erngdvlem4-rN  35305  dvalveclem  35332  dvh0g  35418  dih0cnv  35590  dih1rn  35594  dih1cnv  35595  doch0  35665  doch1  35666  lcfl7lem  35806  mapdheq  36035  hdmap1eq  36109  hdmapval2lem  36141  hgmapvvlem3  36235  mzpval  36313  mzpindd  36327  pellex  36417  2nn0ind  36528  jm2.26lem3  36586  pw2f1o2val  36624  wepwsolem  36630  fnwe2lem3  36640  lnmfg  36670  dgrsub2  36724  mpaaeu  36739  flcidc  36763  rtrclexlem  36942  cnvrcl0  36951  brcoffn  37348  clsk1indlem3  37361  clsneif1o  37422  clsneicnv  37423  clsneikex  37424  clsneinex  37425  neicvgmex  37435  neicvgel1  37437  suprleubrd  37488  suprlubrd  37492  imo72b2  37497  dvconstbi  37555  bcc0  37561  binomcxplemnotnn0  37577  nnfoctb  38238  infleinflem1  38527  fprodcnlem  38666  sumnnodd  38697  icccncfext  38773  itgsin0pilem1  38841  stoweidlem22  38915  stoweidlem32  38925  stoweidlem35  38928  stoweidlem36  38929  stoweidlem37  38930  stoweidlem43  38936  stoweidlem50  38943  wallispilem5  38962  stirlinglem2  38968  stirlinglem3  38969  stirlinglem4  38970  stirlinglem8  38974  stirlinglem11  38977  stirlinglem12  38978  stirlinglem14  38980  stirlinglem15  38981  fourierdlem11  39011  fourierdlem20  39020  fourierdlem21  39021  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem64  39063  fourierdlem71  39070  fourierdlem79  39078  fourierdlem90  39089  fourierdlem91  39090  fourierswlem  39123  etransclem17  39144  etransclem38  39165  meaiininclem  39376  issmflelem  39631  issmfgtlem  39642  issmfgelem  39655  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbnd  40225  pfxid  40255  pfx2  40275  subgrprop3  40500  subgruhgredgd  40508  usgrexi  40661  cusgrexi  40662  cusgrsizeinds  40668  vtxduhgr0e  40693  vtxdgfusgrf  40712  1hevtxdg1  40721  1egrvtxdg1  40725  ewlkprop  40805  1wlklenvm1  40826  1wlkl1loop  40842  1wlkp1lem4  40885  2pthnloop  40937  upgrclwlkcompim  40988  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem6  41018  crctcsh1wlkn0lem7  41019  crctcshlem4  41023  wspthnonp  41055  1wlkpwwlkf1ouspgr  41076  wwlksnwwlksnon  41121  2trld  41145  2spthd  41148  umgr2wlkon  41157  elwwlks2ons3  41159  elwspths2spth  41171  umgrclwwlksge2  41219  wwlksubclwwlks  41232  erclwwlksref  41241  erclwwlksnref  41253  0pthon1-av  41296  11wlkdlem4  41307  1trld  41309  1pthd  41310  3spthd  41343  3cycld  41345  eupth2eucrct  41385  eucrctshift  41411  eucrct2eupth  41413  frgrncvvdeqlemC  41478  frgrhash2wsp  41497  isclintop  41633  clintopcllaw  41637  nzrneg1ne0  41659  rnglz  41674  c0snmgmhm  41704  zrrnghm  41707  lidldomn1  41711  uzlidlring  41719  2zrngnmlid  41739  cznrng  41747  zrinitorngc  41792  zrtermorngc  41793  zrtermoringc  41862  coe1id  41966  blenre  42166  blennn  42167  onsetreclem2  42248