Theorem mpdan 700

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpidan  702  mpan2  704  biadanid  835  mpjaodan  973  mpjao3dan  1459  mpd3an3  1491  elabd2  3627  eueq2  3671  csbiegf  3883  difsnb  4772  reusv3i  5373  frpoinsg  6345  fimadmfo  6802  fimadmfoALT  6804  fvtresfn  6993  fvmpt3  6995  ffvelcdmd  7081  fnressn  7158  fsnex  7287  f1oiso2  7356  riota5f  7401  onsuc  7812  onsucuni  7827  frrlem10  8297  seqomlem2  8443  oaordi  8536  nnaordi  8609  qsdisj  8797  dom2lem  9001  canth2g  9132  limenpsi  9153  nnfi  9165  php4  9207  onfin  9212  sucxpdom  9234  dmfi  9305  fiin  9395  supiso  9449  ordiso2  9490  wdom2d  9555  elirrvOLD  9573  infeq5  9619  cantnfp1lem3  9662  cantnflem1d  9670  rankwflemb  9778  onenon  9957  cardonle  9965  sdomsdomcardi  9979  acni  10051  cardaleph  10095  djuen  10175  djuinf  10194  infdju1  10195  nnadju  10203  pwsdompw  10208  infdif  10213  cfval  10251  fin34  10395  fin1a2lem1  10405  fin1a2  10420  ttukeylem6  10519  sdomsdomcard  10571  canth3  10572  fpwwe2  10655  canthwelem  10662  gchdju1  10668  pwfseqlem4  10674  gchdjuidm  10680  gchxpidm  10681  tskwe2  10785  rankcf  10789  tskuni  10795  gruxp  10819  dmrecnq  10980  lterpq  10982  archnq  10992  reclem3pr  11061  reclem4pr  11062  0idsr  11109  lep1  12083  ledivp1  12144  negfi  12191  supaddc  12209  supmul1  12211  suprzcl  12704  uz11  12915  zmin  12996  zbtwnre  12998  rpnnen1lem4  13032  rpnnen1lem5  13033  xnegid  13292  supxrre  13381  infxrre  13391  eluzfz2  13588  fzsuc  13628  fzsuc2  13639  fzp1disj  13640  fzneuz  13665  nn0p1elfzo  13760  fllep1  13864  fraclt1  13865  fracle1  13866  fracge0  13867  flhalf  13893  ceige  13907  ceim1l  13910  fldiv  13923  modval  13934  suppssfz  14060  seqeq1  14070  expubnd  14244  iexpcyc  14273  binom2sub1  14287  faclbnd4lem3  14361  pfxid  14756  pfxccatpfx2  14808  swrdccat3blem  14810  cshw0  14867  cshwn  14870  cshimadifsn  14902  cshimadifsn0  14903  pfx2  15020  trclexlem  15069  shftfval  15145  shftcan1  15158  sgnneg  15175  reval  15195  cjmulrcl  15233  addcj  15237  absval  15327  absneg  15366  abscj  15368  sqabsadd  15371  sqabssub  15372  leabs  15388  sqreulem  15449  lo1res  15648  o1of2  15702  o1rlimmul  15708  fsumconst1  15879  flo1  15945  trirecip  15954  efcan  16186  efi4p  16229  resin4p  16230  recos4p  16231  sincossq  16268  ruclem10  16331  iddvds  16363  1dvds  16364  2ebits  16541  lcmftp  16730  coprmgcdb  16743  1idssfct  16774  exprmfct  16799  eulerthlem2  16877  odzphi  16892  pcprendvds  16936  pcmpt  16988  oddprmdvds  16999  vdwlem8  17084  0ram2  17117  prmgaplem7  17153  setsn0fun  17269  setsexstruct2  17271  pwsvscaval  17585  2initoinv  18103  initoeu1  18104  initoeu2lem1  18107  initoeu2  18109  2termoinv  18110  termoeu1  18111  homarel  18129  joinfval  18463  meetfval  18477  latjcom  18539  latmcom  18555  0subm  18927  sgrp2nmndlem5  19042  grprcan  19098  isgrpid2  19101  grpinvid  19124  mulgnn0z  19225  qus0  19318  eqg0subg  19325  ghmker  19370  symgbasmap  19505  symginv  19530  pmtrfrn  19586  odmulg2  19683  slwpgp  19741  pj1eq  19828  efgtf  19850  frgpinv  19892  frgpup2  19904  cnaddablx  19996  cnaddabl  19997  zaddablx  20000  imasabl  20004  dprdfadd  20150  dpjidcl  20188  dpjlid  20191  pgpfac1lem3  20207  omndmul2  20261  omndmul  20263  rngen1zr0  20320  srgen1zr0  20356  1unit  20516  unitgrpid  20527  1rinv  20537  irredn0  20565  irredneg  20572  c0snmgmhm  20604  rngisomring1  20610  zrrnghm  20699  rnrhmsubrg  20768  zrinitorngc  20805  zrtermorngc  20806  zrtermoringc  20838  isdrng2  20907  abv0  20990  abv1z  20991  abvneg  20993  orng0le1  21041  lmodfopne  21085  lsssn0  21133  lspsn0  21193  lsp0  21194  lmhmvsca  21230  lmhmrnlss  21235  lmhmkerlss  21236  lsppratlem5  21339  rsp1  21430  kerlidl  21481  ring2idlqus  21513  rngqiprngfulem4  21518  rngqiprngfu  21521  ssdifidllem  21548  cnfldneg  21612  zringcyg  21683  chrid  21739  chrrhm  21745  ip0r  21851  ocvlss  21886  ocv1  21893  rlmassa  22086  psrbagfsupp  22135  snifpsrbag  22136  psrbaglefi  22142  psrvscaval  22166  psrdi  22180  psrdir  22181  mplvscaval  22231  mhpmpl  22373  mhpdeg  22374  mhppwdeg  22379  psdmul  22395  psdpw  22399  coe1sclmulfv  22510  coe1id  22520  evl1var  22562  mamuvs1  22628  mamuvs2  22629  matecl  22648  matvscacell  22659  mat0scmat  22761  submaval0  22803  mdetrsca  22826  maduval  22861  minmar1val0  22870  pmatcollpw3fi1lem2  23013  chcoeffeqlem  23111  cayleyhamilton0  23115  cayleyhamiltonALT  23117  toponsspwpw  23148  cctop  23232  cldval  23249  ntrfval  23250  clsfval  23251  cmclsopn  23288  opncldf3  23312  neifval  23325  lpfval  23364  cnrmnrm  23587  dis2ndc  23687  islocfin  23744  tx1cn  23836  idqtop  23933  kqtopon  23954  kqid  23955  kqcld  23962  hmphen2  24026  filssufil  24139  ufileu  24146  alexsublem  24271  efmndtmd  24328  symgtgp  24333  ustuqtop4  24471  cstucnd  24510  metustexhalf  24783  nm0  24856  rlmnlm  24915  nmolb  24944  metdseq0  25082  pi1xfrval  25283  clmvneg1  25328  clmvsubval  25338  ipcau2  25463  tcphcphlem1  25464  tcphcphlem2  25465  cmetcaulem  25517  ovolicc2lem3  25748  ovolicc2lem4  25749  mbfmulc2lem  25876  i1fpos  25935  mbfi1fseqlem3  25946  itg2ge0  25964  bddiblnc  26071  dvres2  26141  dvaddbr  26167  dvmulbr  26168  dvcobr  26175  dvfsumlem4  26258  ftc1a  26266  ftc1lem6  26270  uc1pmon1p  26379  ig1pval2  26404  dgradd2  26495  dgrcolem2  26501  plydivlem4  26527  plydiveu  26529  elqaalem3  26552  qaa  26554  ulmdvlem1  26633  abelthlem6  26669  abelthlem7  26671  eflogeq  26837  jensenlem2  27222  harmonicbnd4  27245  sgmnncl  27381  dchrptlem2  27499  1lgs  27574  lgs1  27575  2sqcoprm  27669  addsqnreup  27677  dchrisumlem2  27724  dchrisum0lem2a  27751  selberg2lem  27784  pntrsumo1  27799  pntrsumbnd  27800  pntpbnd1  27820  pntlemr  27836  pntlemj  27837  padicabvf  27865  bdayval  27882  noextendgt  27904  nosupbnd2lem1  27949  noinfbnd2lem1  27964  noetainflem4  27974  oldval  28097  divmuls  28484  divscl  28486  seqsp1  28574  bdayfinbndlem1  28730  zz12s  28738  remulscllem1  28763  symquadprlnglem  29042  plngrotlem2  29143  tgaaddcpbllem1  29226  incistruhgr  29522  subgrprop3  29722  subgruhgredgd  29730  usgrexi  29887  cusgrexi  29889  cusgrsizeinds  29898  vtxdgfusgrf  29943  1hevtxdg1  29952  1egrvtxdg1  29955  ewlkprop  30049  wlklenvm1  30067  wlkl1loop  30083  wlkp1lem4  30120  2pthnloop  30182  upgrclwlkcompim  30233  crctcshwlkn0lem4  30267  crctcshwlkn0lem5  30268  crctcshwlkn0lem6  30269  crctcshwlkn0lem7  30270  crctcshlem4  30274  wspthnonp  30313  wlkswwlksf1o  30333  wwlksnwwlksnon  30369  umgr2wlkon  30404  wwlks2onv  30407  elwwlks2ons3im  30408  elwspths2spth  30424  umgrclwwlkge2  30447  clwlkclwwlkf1lem3  30462  erclwwlkref  30476  clwwlknp  30493  wwlksext2clwwlk  30513  wwlksubclwwlk  30514  0pthon1  30584  1wlkdlem4  30596  1pthd  30599  3spthd  30642  eupth2eucrct  30683  eucrctshift  30709  eucrct2eupth  30711  frgrncvvdeqlem8  30772  frgr2wwlkeqm  30797  isgrpoi  30965  grpoinvfval  30989  grpodivfval  31001  vcz  31042  cnaddabloOLD  31048  nvz0  31135  sspz  31202  lno0  31223  nmobndi  31242  ipasslem2  31299  shunssi  31835  ococin  31875  ssjo  31914  pjocini  32165  nlfnval  32348  lncnopbd  32504  riesz3i  32529  cnlnadjlem7  32540  pjclem4  32666  pj3si  32674  hstoc  32689  hstnmoc  32690  hstoh  32699  hst0  32700  mdsl2i  32789  chirredlem3  32859  chirredlem4  32860  dmdbr5ati  32889  rexunirn  32953  fcnvgreu  33132  infxrge0glb  33223  cycpmco2lem5  33557  cycpmco2lem6  33558  cycpmco2lem7  33559  isarchi3  33614  rlocisunit  33703  nsgqusf1olem2  33830  ssmxidllem  33863  rprmdvdspow  33930  ressply1sub  33967  selvply1rhmlemb  34016  fedgmullem1  34126  extdg1id  34163  nn0constr  34258  zartopn  34372  zarcmplem  34378  esumcvg  34583  esumcvgre  34588  sigaval  34608  unelldsys  34656  fiunelros  34672  measval  34696  pmeasmono  34822  probfinmeasb  34926  ballotlemfc0  34991  ballotlemfcc  34992  ballotlemsi  35013  ballotlemfrci  35026  signlem0  35082  breprexp  35128  bnj1006  35456  bnj1110  35478  bnj1253  35513  bnj1280  35516  bnj1463  35551  bnj1312  35554  scottrankeqel  35618  fineqvinfep  35638  erdszelem7  35763  erdszelem8  35764  cvmliftlem10  35860  cvmliftlem13  35862  cvmlift2lem9  35877  cvmlift3lem6  35890  cvmlift3lem7  35891  cvmlift3lem9  35893  satfv1lem  35928  dfrdg2  36359  cldregopn  36937  tailfval  36978  filnetlem3  36986  filnetlem4  36987  ontopbas  37034  bj-nnfbd  37489  bj-elid4  37907  bj-imdiridlem  37924  f1omptsnlem  38077  icoreunrn  38100  relowlpssretop  38105  fvineqsnf1  38151  wl-sbal2  38314  unccur  38344  poimirlem1  38357  poimirlem2  38358  poimirlem4  38360  poimirlem6  38362  poimirlem7  38363  poimirlem11  38367  poimirlem12  38368  poimirlem17  38373  poimirlem20  38376  poimirlem22  38378  poimirlem23  38379  poimirlem28  38384  poimir  38389  ismblfin  38397  cnambfre  38404  ftc1cnnc  38428  dvasin  38440  ismtyres  38545  heiborlem8  38555  ghomidOLD  38626  rngosn6  38663  rngonegmn1l  38678  rngonegmn1r  38679  rngoneglmul  38680  rngonegrmul  38681  idlnegcl  38759  0idl  38762  0rngo  38764  smprngopr  38789  sucmapsuc  39224  cossex  39244  qsdisjALTV  39434  cnvepresdmqss  39472  mpets2  39690  lkrval  39948  ldualvaddval  39991  ldualvsval  39998  opoc1  40062  pmap0  40625  pmap1N  40627  pexmidALTN  40838  cdleme31fv  41250  cdlemg27b  41556  erngdvlem4  41851  erng0g  41854  erngdvlem4-rN  41859  dvalveclem  41885  dvh0g  41971  dih0cnv  42143  dih1rn  42147  dih1cnv  42148  doch0  42218  doch1  42219  lcfl7lem  42359  mapdheq  42588  hdmap1eq  42661  hdmapval2lem  42691  hgmapvvlem3  42785  zndvdchrrhm  42826  lcmineqlem13  42894  aks4d1p9  42941  primrootsunit1  42950  aks6d1c1p1  42960  aks6d1c1p6  42967  aks6d1c1p8  42968  sticksstones1  42999  sticksstones6  43004  sticksstones7  43005  sticksstones11  43009  sticksstones12a  43010  sticksstones12  43011  sticksstones22  43021  aks6d1c6isolem1  43027  aks6d1c6isolem2  43028  unitscyglem5  43052  renegid  43235  sn-0ne2  43268  remul01  43269  remulinvcom  43295  sn-0tie0  43326  renegmulnnass  43340  domnexpgn0cl  43392  abvexp  43401  frlmsnic  43409  fsuppssind  43426  mzpval  43564  mzpindd  43578  pellex  43663  2nn0ind  43773  jm2.26lem3  43829  pw2f1o2val  43867  wepwsolem  43870  fnwe2lem3  43880  lnmfg  43910  dgrsub2  43963  mpaaeu  43978  flcidc  43998  dflim5  44157  naddwordnexlem1  44225  rtrclexlem  44443  cnvrcl0  44452  brcoffn  44857  clsk1indlem3  44870  clsneif1o  44931  clsneicnv  44932  clsneikex  44933  clsneinex  44934  neicvgmex  44944  neicvgel1  44946  suprleubrd  44993  suprlubrd  44995  imo72b2  44999  dvconstbi  45145  bcc0  45151  binomcxplemnotnn0  45167  nnfoctb  45869  infleinflem1  46186  fprodcnlem  46416  sumnnodd  46447  icccncfext  46702  itgsin0pilem1  46765  stoweidlem32  46847  stoweidlem35  46850  stoweidlem36  46851  stoweidlem37  46852  stoweidlem43  46858  stoweidlem50  46865  wallispilem5  46884  stirlinglem2  46890  stirlinglem3  46891  stirlinglem4  46892  stirlinglem8  46896  stirlinglem11  46899  stirlinglem12  46900  stirlinglem14  46902  stirlinglem15  46903  fourierdlem11  46933  fourierdlem20  46942  fourierdlem21  46943  fourierdlem41  46963  fourierdlem42  46964  fourierdlem48  46969  fourierdlem49  46970  fourierdlem64  46985  fourierdlem71  46992  fourierdlem79  47000  fourierdlem90  47011  fourierdlem91  47012  fourierswlem  47045  etransclem17  47066  etransclem38  47087  saluni  47140  meaiininclem  47301  issmflelem  47559  issmfgtlem  47570  issmfgelem  47584  smflimsuplem4  47638  sqrtnnaa  47718  f1cof1blem  47949  zplusmodne  48224  m1modne  48229  submodneaddmod  48232  nndivides2  48259  sprval  48366  prprval  48401  bgoldbtbndlem2  48709  bgoldbtbndlem3  48710  bgoldbtbnd  48712  isubgrvtxuhgr  48767  isubgredg  48769  grimcnv  48791  isuspgrim  48799  gricushgr  48820  uhgrimisgrgric  48834  grtriclwlk3  48848  isubgr3stgrlem7  48875  grlimgrtri  48906  grlictr  48918  gpgvtx0  48956  gpgvtx1  48957  gpgprismgrusgra  48961  gpgedgvtx1  48965  gpg3kgrtriex  48992  pgnbgreunbgrlem3  49021  pgnbgreunbgrlem6  49027  isclintop  49109  clintopcllaw  49113  nzrneg1ne0  49132  lidldomn1  49133  zlidlring  49136  uzlidlring  49137  2zrngnmlid  49157  cznrng  49163  blenre  49491  blennn  49492  2arymaptf  49569  itcoval1  49580  itcovalendof  49586  ehl2eudisval0  49642  eenglngeehlnmlem2  49655  itsclc0yqsol  49681  inlinecirc02plem  49703  ipolub  49901  ipoglb  49904  nelsubclem  49980  imaid  50067  imaf1co  50068  uptri  50127  uptrar  50129  uptrai  50130  oppc1stflem  50200  setrec2mpt  50610