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  3623  eueq2  3667  csbiegf  3879  difsnb  4768  reusv3i  5365  frpoinsg  6346  fimadmfo  6805  fimadmfoALT  6807  fvtresfn  6996  fvmpt3  6998  ffvelcdmd  7085  fnressn  7162  fsnex  7291  f1oiso2  7360  riota5f  7405  onsuc  7824  onsucuni  7839  fnwe2lem4  8148  frrlem10  8313  seqomlem2  8461  oaordi  8554  nnaordi  8627  qsdisj  8815  dom2lem  9019  canth2g  9150  limenpsi  9171  nnfi  9183  php4  9225  onfin  9230  sucxpdom  9252  dmfi  9324  fiin  9414  supiso  9468  ordiso2  9509  wdom2d  9574  elirrvOLD  9592  infeq5  9638  cantnfp1lem3  9681  cantnflem1d  9689  rankwflemb  9800  rankwflembOLD  9801  onenon  10030  cardonle  10038  sdomsdomcardi  10052  acni  10124  cardaleph  10168  djuen  10248  djuinf  10267  infdju1  10268  nnadju  10276  pwsdompw  10281  infdif  10286  cfval  10324  fin34  10468  fin1a2lem1  10478  fin1a2  10493  ttukeylem6  10592  sdomsdomcard  10644  canth3  10645  fpwwe2  10728  canthwelem  10735  gchdju1  10741  pwfseqlem4  10747  gchdjuidm  10753  gchxpidm  10754  tskwe2  10858  rankcf  10862  tskuni  10868  gruxp  10892  dmrecnq  11053  lterpq  11055  archnq  11065  reclem3pr  11134  reclem4pr  11135  0idsr  11182  lep1  12158  ledivp1  12219  negfi  12266  supaddc  12284  supmul1  12286  suprzcl  12779  uz11  12990  zmin  13071  zbtwnre  13073  rpnnen1lem4  13108  rpnnen1lem5  13109  xnegid  13368  supxrre  13457  infxrre  13467  eluzfz2  13665  fzsuc  13705  fzsuc2  13716  fzp1disj  13717  fzneuz  13742  nn0p1elfzo  13837  fllep1  13941  fraclt1  13942  fracle1  13943  fracge0  13944  flhalf  13970  ceige  13984  ceim1l  13987  fldiv  14000  modval  14011  suppssfz  14137  seqeq1  14147  expubnd  14321  iexpcyc  14351  binom2sub1  14365  faclbnd4lem3  14439  pfxid  14834  pfxccatpfx2  14886  swrdccat3blem  14888  cshw0  14945  cshwn  14948  cshimadifsn  14980  cshimadifsn0  14981  pfx2  15098  trclexlem  15147  shftfval  15223  shftcan1  15236  sgnneg  15253  reval  15273  cjmulrcl  15311  addcj  15315  absval  15405  absneg  15444  abscj  15446  sqabsadd  15449  sqabssub  15450  leabs  15466  sqreulem  15527  lo1res  15726  o1of2  15780  o1rlimmul  15786  fsumconst1  15957  flo1  16023  trirecip  16032  efcan  16262  efi4p  16305  resin4p  16306  recos4p  16307  sincossq  16344  ruclem10  16407  iddvds  16439  1dvds  16440  2ebits  16617  lcmftp  16811  coprmgcdb  16824  1idssfct  16855  exprmfct  16880  eulerthlem2  16959  odzphi  16974  pcprendvds  17018  pcmpt  17070  oddprmdvds  17081  vdwlem8  17166  0ram2  17199  prmgaplem7  17235  setsn0fun  17351  setsexstruct2  17353  pwsvscaval  17667  2initoinv  18185  initoeu1  18186  initoeu2lem1  18189  initoeu2  18191  2termoinv  18192  termoeu1  18193  homarel  18211  joinfval  18545  meetfval  18559  latjcom  18621  latmcom  18637  0subm  19013  sgrp2nmndlem5  19128  grprcan  19184  isgrpid2  19187  grpinvid  19210  mulgnn0z  19311  qus0  19404  eqg0subg  19411  ghmker  19456  symgbasmap  19591  symginv  19616  pmtrfrn  19672  odmulg2  19769  slwpgp  19827  pj1eq  19914  efgtf  19936  frgpinv  19978  frgpup2  19990  cnaddablx  20082  cnaddabl  20083  zaddablx  20086  imasabl  20090  dprdfadd  20236  dpjidcl  20274  dpjlid  20277  pgpfac1lem3  20293  omndmul2  20347  omndmul  20349  rngen1zr0  20406  srgen1zr0  20442  1unit  20604  unitgrpid  20615  1rinv  20625  irredn0  20653  irredneg  20660  c0snmgmhm  20692  rngisomring1  20698  zrrnghm  20788  rnrhmsubrg  20857  zrinitorngc  20894  zrtermorngc  20895  zrtermoringc  20927  isdrng2  20997  abv0  21080  abv1z  21081  abvneg  21083  orng0le1  21131  lmodfopne  21175  lsssn0  21223  lspsn0  21283  lsp0  21284  lmhmvsca  21320  lmhmrnlss  21325  lmhmkerlss  21326  lsppratlem5  21429  rsp1  21520  kerlidl  21572  ring2idlqus  21605  rngqiprngfulem4  21610  rngqiprngfu  21613  ssdifidllem  21640  cnfldneg  21704  zringcyg  21775  chrid  21831  chrrhm  21837  ip0r  21943  ocvlss  21978  ocv1  21985  rlmassa  22178  psrbagfsupp  22227  snifpsrbag  22228  psrbaglefi  22234  psrvscaval  22258  psrdi  22272  psrdir  22273  mplvscaval  22323  mhpmpl  22465  mhpdeg  22466  mhppwdeg  22471  psdmul  22487  psdpw  22491  coe1sclmulfv  22602  coe1id  22612  evl1var  22654  mamuvs1  22720  mamuvs2  22721  matecl  22740  matvscacell  22751  mat0scmat  22853  submaval0  22895  mdetrsca  22918  maduval  22953  minmar1val0  22962  pmatcollpw3fi1lem2  23105  chcoeffeqlem  23203  cayleyhamilton0  23207  cayleyhamiltonALT  23209  toponsspwpw  23240  cctop  23324  cldval  23341  ntrfval  23342  clsfval  23343  cmclsopn  23380  opncldf3  23404  neifval  23417  lpfval  23456  cnrmnrm  23679  dis2ndc  23779  islocfin  23836  tx1cn  23928  idqtop  24025  kqtopon  24046  kqid  24047  kqcld  24054  hmphen2  24118  filssufil  24231  ufileu  24238  alexsublem  24363  efmndtmd  24420  symgtgp  24425  ustuqtop4  24563  cstucnd  24602  metustexhalf  24875  nm0  24948  rlmnlm  25007  nmolb  25036  metdseq0  25174  pi1xfrval  25375  clmvneg1  25420  clmvsubval  25430  ipcau2  25555  tcphcphlem1  25556  tcphcphlem2  25557  cmetcaulem  25609  ovolicc2lem3  25840  ovolicc2lem4  25841  mbfmulc2lem  25968  i1fpos  26027  mbfi1fseqlem3  26038  itg2ge0  26056  bddiblnc  26162  dvres2  26232  dvaddbr  26258  dvmulbr  26259  dvcobr  26266  dvfsumlem4  26349  ftc1a  26357  ftc1lem6  26361  uc1pmon1p  26470  ig1pval2  26495  dgradd2  26587  dgrcolem2  26593  plydivlem4  26617  plydiveu  26619  rnplynfin  26630  elqaalem3  26644  qaa  26647  ulmdvlem1  26727  abelthlem6  26763  abelthlem7  26765  eflogeq  26930  jensenlem2  27315  harmonicbnd4  27338  sgmnncl  27474  dchrptlem2  27592  1lgs  27667  lgs1  27668  2sqcoprm  27762  addsqnreup  27770  dchrisumlem2  27817  dchrisum0lem2a  27844  selberg2lem  27877  pntrsumo1  27892  pntrsumbnd  27893  pntpbnd1  27913  pntlemr  27929  pntlemj  27930  padicabvf  27958  bdayval  28005  noextendgt  28027  nosupbnd2lem1  28072  noinfbnd2lem1  28087  noetainflem4  28097  oldval  28220  divmuls  28607  divscl  28609  seqsp1  28697  bdayfinbndlem1  28853  zz12s  28861  remulscllem1  28886  symquadprlnglem  29165  plngrotlem2  29266  tgaaddcpbllem1  29349  incistruhgr  29657  subgrprop3  29857  subgruhgredgd  29865  usgrexi  30022  cusgrexi  30024  cusgrsizeinds  30033  vtxdgfusgrf  30078  1hevtxdg1  30087  1egrvtxdg1  30090  ewlkprop  30184  wlklenvm1  30202  wlkl1loop  30218  wlkp1lem4  30255  2pthnloop  30317  upgrclwlkcompim  30368  crctcshwlkn0lem4  30402  crctcshwlkn0lem5  30403  crctcshwlkn0lem6  30404  crctcshwlkn0lem7  30405  crctcshlem4  30409  wspthnonp  30448  wlkswwlksf1o  30468  wwlksnwwlksnon  30504  umgr2wlkon  30539  wwlks2onv  30542  elwwlks2ons3im  30543  elwspths2spth  30559  umgrclwwlkge2  30582  clwlkclwwlkf1lem3  30597  erclwwlkref  30611  clwwlknp  30628  wwlksext2clwwlk  30648  wwlksubclwwlk  30649  0pthon1  30719  1wlkdlem4  30731  1pthd  30734  3spthd  30777  eupth2eucrct  30818  eucrctshift  30844  eucrct2eupth  30846  frgrncvvdeqlem8  30907  frgr2wwlkeqm  30932  isgrpoi  31100  grpoinvfval  31124  grpodivfval  31136  vcz  31177  cnaddabloOLD  31183  nvz0  31270  sspz  31337  lno0  31358  nmobndi  31377  ipasslem2  31434  shunssi  31970  ococin  32010  ssjo  32049  pjocini  32300  nlfnval  32483  lncnopbd  32639  riesz3i  32664  cnlnadjlem7  32675  pjclem4  32801  pj3si  32809  hstoc  32824  hstnmoc  32825  hstoh  32834  hst0  32835  mdsl2i  32924  chirredlem3  32994  chirredlem4  32995  dmdbr5ati  33024  rexunirn  33130  fcnvgreu  33308  infxrge0glb  33399  cycpmco2lem5  33733  cycpmco2lem6  33734  cycpmco2lem7  33735  isarchi3  33790  rlocisunit  33879  nsgqusf1olem2  34007  ssmxidllem  34040  rprmdvdspow  34107  ressply1sub  34144  selvply1rhmlemb  34193  fedgmullem1  34303  extdg1id  34340  nn0constr  34435  zartopn  34549  zarcmplem  34555  esumcvg  34760  esumcvgre  34765  sigaval  34785  unelldsys  34833  fiunelros  34849  measval  34873  pmeasmono  34998  probfinmeasb  35102  ballotlemfc0  35167  ballotlemfcc  35168  ballotlemsi  35189  ballotlemfrci  35202  signlem0  35258  breprexp  35304  bnj1006  35632  bnj1110  35654  bnj1253  35689  bnj1280  35692  bnj1463  35727  bnj1312  35730  scottrankeqel  35790  fineqvinfep  35835  erdszelem7  36004  erdszelem8  36005  cvmliftlem10  36101  cvmliftlem13  36103  cvmlift2lem9  36118  cvmlift3lem6  36131  cvmlift3lem7  36132  cvmlift3lem9  36134  satfv1lem  36169  dfrdg2  36599  cldregopn  37161  tailfval  37202  filnetlem3  37210  filnetlem4  37211  ontopbas  37258  bj-nnfbd  37713  bj-elid4  38132  bj-imdiridlem  38149  f1omptsnlem  38302  icoreunrn  38325  relowlpssretop  38330  fvineqsnf1  38376  wl-sbal2  38539  unccur  38569  poimirlem1  38582  poimirlem2  38583  poimirlem4  38585  poimirlem6  38587  poimirlem7  38588  poimirlem11  38592  poimirlem12  38593  poimirlem17  38598  poimirlem20  38601  poimirlem22  38603  poimirlem23  38604  poimirlem28  38609  poimir  38614  ismblfin  38622  cnambfre  38629  ftc1cnnc  38653  dvasin  38665  ismtyres  38785  heiborlem8  38795  ghomidOLD  38866  rngosn6  38903  rngonegmn1l  38918  rngonegmn1r  38919  rngoneglmul  38920  rngonegrmul  38921  idlnegcl  38999  0idl  39002  0rngo  39004  smprngopr  39029  sucmapsuc  39464  cossex  39484  qsdisjALTV  39674  cnvepresdmqss  39712  mpets2  39930  lkrval  40188  ldualvaddval  40231  ldualvsval  40238  opoc1  40302  pmap0  40865  pmap1N  40867  pexmidALTN  41078  cdleme31fv  41490  cdlemg27b  41796  erngdvlem4  42091  erng0g  42094  erngdvlem4-rN  42099  dvalveclem  42125  dvh0g  42211  dih0cnv  42383  dih1rn  42387  dih1cnv  42388  doch0  42458  doch1  42459  lcfl7lem  42599  mapdheq  42828  hdmap1eq  42901  hdmapval2lem  42931  hgmapvvlem3  43025  zndvdchrrhm  43066  lcmineqlem13  43134  aks4d1p9  43181  primrootsunit1  43190  aks6d1c1p1  43200  aks6d1c1p6  43207  aks6d1c1p8  43208  sticksstones1  43239  sticksstones6  43244  sticksstones7  43245  sticksstones11  43249  sticksstones12a  43250  sticksstones12  43251  sticksstones22  43261  aks6d1c6isolem1  43267  aks6d1c6isolem2  43268  unitscyglem5  43292  renegid  43467  sn-0ne2  43500  remul01  43501  remulinvcom  43527  sn-0tie0  43558  renegmulnnass  43572  domnexpgn0cl  43627  abvexp  43639  frlmsnic  43647  fsuppssind  43664  mzpval  43786  mzpindd  43800  pellex  43885  2nn0ind  43995  jm2.26lem3  44051  pw2f1o2val  44089  wepwsolem  44092  lnmfg  44127  dgrsub2  44180  mpaaeu  44195  flcidc  44215  dflim5  44374  naddwordnexlem1  44442  rtrclexlem  44659  cnvrcl0  44668  brcoffn  45073  clsk1indlem3  45086  clsneif1o  45147  clsneicnv  45148  clsneikex  45149  clsneinex  45150  neicvgmex  45160  neicvgel1  45162  suprleubrd  45209  suprlubrd  45211  imo72b2  45215  dvconstbi  45361  bcc0  45367  binomcxplemnotnn0  45383  nnfoctb  46108  infleinflem1  46424  fprodcnlem  46654  sumnnodd  46685  icccncfext  46940  itgsin0pilem1  47003  stoweidlem32  47085  stoweidlem35  47088  stoweidlem36  47089  stoweidlem37  47090  stoweidlem43  47096  stoweidlem50  47103  wallispilem5  47122  stirlinglem2  47128  stirlinglem3  47129  stirlinglem4  47130  stirlinglem8  47134  stirlinglem11  47137  stirlinglem12  47138  stirlinglem14  47140  stirlinglem15  47141  fourierdlem11  47171  fourierdlem20  47180  fourierdlem21  47181  fourierdlem41  47201  fourierdlem42  47202  fourierdlem48  47207  fourierdlem49  47208  fourierdlem64  47223  fourierdlem71  47230  fourierdlem79  47238  fourierdlem90  47249  fourierdlem91  47250  fourierswlem  47283  etransclem17  47304  etransclem38  47325  saluni  47378  meaiininclem  47539  issmflelem  47797  issmfgtlem  47808  issmfgelem  47822  smflimsuplem4  47876  sqrtnnaa  47956  f1cof1blem  48187  zplusmodne  48462  m1modne  48467  submodneaddmod  48470  nndivides2  48497  sprval  48604  prprval  48639  bgoldbtbndlem2  48947  bgoldbtbndlem3  48948  bgoldbtbnd  48950  isubgrvtxuhgr  49005  isubgredg  49007  grimcnv  49029  isuspgrim  49037  gricushgr  49058  uhgrimisgrgric  49072  grtriclwlk3  49086  isubgr3stgrlem7  49113  grlimgrtri  49144  grlictr  49156  gpgvtx0  49194  gpgvtx1  49195  gpgprismgrusgra  49199  gpgedgvtx1  49203  gpg3kgrtriex  49230  pgnbgreunbgrlem3  49259  pgnbgreunbgrlem6  49265  isclintop  49347  clintopcllaw  49351  nzrneg1ne0  49370  lidldomn1  49371  zlidlring  49374  uzlidlring  49375  2zrngnmlid  49395  cznrng  49401  blenre  49729  blennn  49730  2arymaptf  49807  itcoval1  49818  itcovalendof  49824  ehl2eudisval0  49880  eenglngeehlnmlem2  49893  itsclc0yqsol  49919  inlinecirc02plem  49941  ipolub  50139  ipoglb  50142  nelsubclem  50218  imaid  50305  imaf1co  50306  uptri  50365  uptrar  50367  uptrai  50368  oppc1stflem  50438  setrec2mpt  50833