Theorem mpdan 688

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 585	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 207  df-an 396

This theorem is referenced by:  mpidan  690  mpan2  692  biadanid  823  mpjaodan  961  mpjao3dan  1435  mpd3an3  1465  elabd2  3610  eueq2  3653  csbiegf  3866  difsnb  4741  reusv3i  5335  frpoinsg  6296  fimadmfo  6750  fimadmfoALT  6752  fvtresfn  6939  fvmpt3  6941  ffvelcdmd  7026  fnressn  7101  fsnex  7227  f1oiso2  7296  riota5f  7341  onsuc  7753  onsucuni  7768  frrlem10  8234  seqomlem2  8379  oaordi  8470  nnaordi  8543  qsdisj  8730  dom2lem  8928  canth2g  9058  limenpsi  9079  nnfi  9091  php4  9133  onfin  9138  sucxpdom  9160  dmfi  9234  fiin  9324  supiso  9378  ordiso2  9419  wdom2d  9484  elirrv  9501  infeq5  9547  cantnfp1lem3  9590  cantnflem1d  9598  rankwflemb  9706  onenon  9862  cardonle  9870  sdomsdomcardi  9884  acni  9956  cardaleph  10000  djuen  10081  djuinf  10100  infdju1  10101  nnadju  10109  pwsdompw  10114  infdif  10119  cfval  10158  fin34  10301  fin1a2lem1  10311  fin1a2  10326  ttukeylem6  10425  sdomsdomcard  10471  canth3  10472  fpwwe2  10555  canthwelem  10562  gchdju1  10568  pwfseqlem4  10574  gchdjuidm  10580  gchxpidm  10581  tskwe2  10685  rankcf  10689  tskuni  10695  gruxp  10719  dmrecnq  10880  lterpq  10882  archnq  10892  reclem3pr  10961  reclem4pr  10962  0idsr  11009  lep1  11985  ledivp1  12047  negfi  12094  supaddc  12112  supmul1  12114  suprzcl  12598  uz11  12802  zmin  12883  zbtwnre  12885  rpnnen1lem4  12919  rpnnen1lem5  12920  xnegid  13179  supxrre  13268  infxrre  13278  eluzfz2  13475  fzsuc  13514  fzsuc2  13525  fzp1disj  13526  fzneuz  13551  nn0p1elfzo  13646  fllep1  13749  fraclt1  13750  fracle1  13751  fracge0  13752  flhalf  13778  ceige  13792  ceim1l  13795  fldiv  13808  modval  13819  suppssfz  13945  seqeq1  13955  expubnd  14129  iexpcyc  14158  binom2sub1  14172  faclbnd4lem3  14246  pfxid  14636  pfxccatpfx2  14688  swrdccat3blem  14690  cshw0  14745  cshwn  14748  cshimadifsn  14780  cshimadifsn0  14781  pfx2  14898  trclexlem  14945  shftfval  15021  shftcan1  15034  reval  15057  cjmulrcl  15095  addcj  15099  absval  15189  absneg  15228  abscj  15230  sqabsadd  15233  sqabssub  15234  leabs  15250  sqreulem  15311  lo1res  15510  o1of2  15564  o1rlimmul  15570  fsumconst1  15742  flo1  15808  trirecip  15817  efcan  16050  efi4p  16093  resin4p  16094  recos4p  16095  sincossq  16132  ruclem10  16195  iddvds  16227  1dvds  16228  2ebits  16405  lcmftp  16594  coprmgcdb  16607  1idssfct  16638  exprmfct  16663  eulerthlem2  16741  odzphi  16756  pcprendvds  16800  pcmpt  16852  oddprmdvds  16863  vdwlem8  16948  0ram2  16981  prmgaplem7  17017  setsn0fun  17132  setsexstruct2  17134  pwsvscaval  17448  2initoinv  17966  initoeu1  17967  initoeu2lem1  17970  initoeu2  17972  2termoinv  17973  termoeu1  17974  homarel  17992  joinfval  18326  meetfval  18340  latjcom  18402  latmcom  18418  0subm  18774  sgrp2nmndlem5  18889  grprcan  18938  isgrpid2  18941  grpinvid  18964  mulgnn0z  19066  qus0  19153  eqg0subg  19160  ghmker  19206  symgbasmap  19341  symginv  19366  pmtrfrn  19422  odmulg2  19519  slwpgp  19577  pj1eq  19664  efgtf  19686  frgpinv  19728  frgpup2  19740  cnaddablx  19832  cnaddabl  19833  zaddablx  19836  imasabl  19840  dprdfadd  19986  dpjidcl  20024  dpjlid  20027  pgpfac1lem3  20043  omndmul2  20097  omndmul  20099  srgen1zr  20186  1unit  20343  unitgrpid  20354  1rinv  20364  irredn0  20392  irredneg  20399  c0snmgmhm  20431  rngisomring1  20437  zrrnghm  20502  rnrhmsubrg  20571  zrinitorngc  20608  zrtermorngc  20609  zrtermoringc  20641  isdrng2  20709  ringen1zr  20744  abv0  20789  abv1z  20790  abvneg  20792  orng0le1  20840  lmodfopne  20884  lsssn0  20932  lspsn0  20992  lsp0  20993  lmhmvsca  21029  lmhmrnlss  21034  lmhmkerlss  21035  lsppratlem5  21138  rsp1  21224  kerlidl  21265  ring2idlqus  21296  rngqiprngfulem4  21301  rngqiprngfu  21304  cnfldneg  21367  zringcyg  21438  chrid  21494  chrrhm  21500  ip0r  21606  ocvlss  21641  ocv1  21648  rlmassa  21839  psrbagfsupp  21888  snifpsrbag  21889  psrbaglefi  21895  psrvscaval  21918  psrdi  21932  psrdir  21933  mplvscaval  21983  mhpmpl  22099  mhpdeg  22100  mhppwdeg  22105  psdmul  22121  psdpw  22125  coe1sclmulfv  22236  coe1id  22246  ply1idvr1OLD  22248  evl1var  22289  mamuvs1  22358  mamuvs2  22359  matecl  22378  matvscacell  22389  mat0scmat  22491  submaval0  22533  mdetrsca  22556  maduval  22591  minmar1val0  22600  pmatcollpw3fi1lem2  22740  chcoeffeqlem  22838  cayleyhamilton0  22842  cayleyhamiltonALT  22844  toponsspwpw  22875  cctop  22959  cldval  22976  ntrfval  22977  clsfval  22978  cmclsopn  23015  opncldf3  23039  neifval  23052  lpfval  23091  cnrmnrm  23314  dis2ndc  23413  islocfin  23470  tx1cn  23562  idqtop  23659  kqtopon  23680  kqid  23681  kqcld  23688  hmphen2  23752  filssufil  23865  ufileu  23872  alexsublem  23997  efmndtmd  24054  symgtgp  24059  ustuqtop4  24197  cstucnd  24236  metustexhalf  24509  nm0  24582  rlmnlm  24641  nmolb  24670  metdseq0  24808  pi1xfrval  25009  clmvneg1  25054  clmvsubval  25064  ipcau2  25189  tcphcphlem1  25190  tcphcphlem2  25191  cmetcaulem  25243  ovolicc2lem3  25474  ovolicc2lem4  25475  mbfmulc2lem  25602  i1fpos  25661  mbfi1fseqlem3  25672  itg2ge0  25690  bddiblnc  25797  dvres2  25867  dvaddbr  25893  dvmulbr  25894  dvcobr  25901  dvfsumlem4  25984  ftc1a  25992  ftc1lem6  25996  uc1pmon1p  26105  ig1pval2  26130  dgradd2  26221  dgrcolem2  26227  plydivlem4  26250  plydiveu  26252  elqaalem3  26275  qaa  26277  ulmdvlem1  26353  abelthlem6  26389  abelthlem7  26391  eflogeq  26554  jensenlem2  26939  harmonicbnd4  26962  sgmnncl  27098  dchrptlem2  27216  1lgs  27291  lgs1  27292  2sqcoprm  27386  addsqnreup  27394  dchrisumlem2  27441  dchrisum0lem2a  27468  selberg2lem  27501  pntrsumo1  27516  pntrsumbnd  27517  pntpbnd1  27537  pntlemr  27553  pntlemj  27554  padicabvf  27582  bdayval  27600  noextendgt  27622  nosupbnd2lem1  27667  noinfbnd2lem1  27682  noetainflem4  27692  oldval  27814  divmuls  28201  divscl  28203  seqsp1  28291  bdayfinbndlem1  28447  zz12s  28455  remulscllem1  28480  incistruhgr  29136  subgrprop3  29333  subgruhgredgd  29341  usgrexi  29498  cusgrexi  29500  cusgrsizeinds  29509  vtxdgfusgrf  29554  1hevtxdg1  29563  1egrvtxdg1  29566  ewlkprop  29660  wlklenvm1  29678  wlkl1loop  29694  wlkp1lem4  29731  2pthnloop  29787  upgrclwlkcompim  29837  crctcshwlkn0lem4  29869  crctcshwlkn0lem5  29870  crctcshwlkn0lem6  29871  crctcshwlkn0lem7  29872  crctcshlem4  29876  wspthnonp  29915  wlkswwlksf1o  29935  wwlksnwwlksnon  29971  umgr2wlkon  30006  wwlks2onv  30009  elwwlks2ons3im  30010  elwspths2spth  30026  umgrclwwlkge2  30049  clwlkclwwlkf1lem3  30064  erclwwlkref  30078  clwwlknp  30095  wwlksext2clwwlk  30115  wwlksubclwwlk  30116  0pthon1  30186  1wlkdlem4  30198  1pthd  30201  3spthd  30234  eupth2eucrct  30275  eucrctshift  30301  eucrct2eupth  30303  frgrncvvdeqlem8  30364  frgr2wwlkeqm  30389  isgrpoi  30557  grpoinvfval  30581  grpodivfval  30593  vcz  30634  cnaddabloOLD  30640  nvz0  30727  sspz  30794  lno0  30815  nmobndi  30834  ipasslem2  30891  shunssi  31427  ococin  31467  ssjo  31506  pjocini  31757  nlfnval  31940  lncnopbd  32096  riesz3i  32121  cnlnadjlem7  32132  pjclem4  32258  pj3si  32266  hstoc  32281  hstnmoc  32282  hstoh  32291  hst0  32292  mdsl2i  32381  chirredlem3  32451  chirredlem4  32452  dmdbr5ati  32481  rexunirn  32549  fcnvgreu  32733  infxrge0glb  32826  sgnneg  32894  cycpmco2lem5  33179  cycpmco2lem6  33180  cycpmco2lem7  33181  isarchi3  33236  nsgqusf1olem2  33462  ssdifidllem  33504  ssmxidllem  33521  rprmdvdspow  33581  ressply1sub  33618  fedgmullem1  33761  extdg1id  33798  nn0constr  33893  zartopn  34007  zarcmplem  34013  esumcvg  34218  esumcvgre  34223  sigaval  34243  unelldsys  34290  fiunelros  34306  measval  34330  pmeasmono  34456  probfinmeasb  34560  ballotlemfc0  34625  ballotlemfcc  34626  ballotlemsi  34647  ballotlemfrci  34660  signlem0  34719  breprexp  34765  bnj1006  35090  bnj1110  35112  bnj1253  35147  bnj1280  35150  bnj1463  35185  bnj1312  35188  fineqvinfep  35257  erdszelem7  35367  erdszelem8  35368  cvmliftlem10  35464  cvmliftlem13  35466  cvmlift2lem9  35481  cvmlift3lem6  35494  cvmlift3lem7  35495  cvmlift3lem9  35497  satfv1lem  35532  dfrdg2  35963  cldregopn  36501  tailfval  36542  filnetlem3  36550  filnetlem4  36551  ontopbas  36598  bj-nnfbd  37054  bj-elid4  37470  bj-imdiridlem  37487  f1omptsnlem  37640  icoreunrn  37663  relowlpssretop  37668  fvineqsnf1  37714  wl-sbal2  37877  unccur  37912  poimirlem1  37930  poimirlem2  37931  poimirlem4  37933  poimirlem6  37935  poimirlem7  37936  poimirlem11  37940  poimirlem12  37941  poimirlem17  37946  poimirlem20  37949  poimirlem22  37951  poimirlem23  37952  poimirlem28  37957  poimir  37962  ismblfin  37970  cnambfre  37977  ftc1cnnc  38001  dvasin  38013  ismtyres  38117  heiborlem8  38127  ghomidOLD  38198  rngosn6  38235  rngonegmn1l  38250  rngonegmn1r  38251  rngoneglmul  38252  rngonegrmul  38253  idlnegcl  38331  0idl  38334  0rngo  38336  smprngopr  38361  sucmapsuc  38798  cossex  38818  qsdisjALTV  39008  cnvepresdmqss  39046  mpets2  39264  lkrval  39522  ldualvaddval  39565  ldualvsval  39572  opoc1  39636  pmap0  40199  pmap1N  40201  pexmidALTN  40412  cdleme31fv  40824  cdlemg27b  41130  erngdvlem4  41425  erng0g  41428  erngdvlem4-rN  41433  dvalveclem  41459  dvh0g  41545  dih0cnv  41717  dih1rn  41721  dih1cnv  41722  doch0  41792  doch1  41793  lcfl7lem  41933  mapdheq  42162  hdmap1eq  42235  hdmapval2lem  42265  hgmapvvlem3  42359  zndvdchrrhm  42400  lcmineqlem13  42468  aks4d1p9  42515  primrootsunit1  42524  aks6d1c1p1  42534  aks6d1c1p6  42541  aks6d1c1p8  42542  sticksstones1  42573  sticksstones6  42578  sticksstones7  42579  sticksstones11  42583  sticksstones12a  42584  sticksstones12  42585  sticksstones22  42595  aks6d1c6isolem1  42601  aks6d1c6isolem2  42602  unitscyglem5  42626  renegid  42793  sn-0ne2  42826  remul01  42827  remulinvcom  42853  sn-0tie0  42884  renegmulnnass  42898  domnexpgn0cl  42956  abvexp  42965  frlmsnic  42973  fsuppssind  43014  mzpval  43152  mzpindd  43166  pellex  43251  2nn0ind  43361  jm2.26lem3  43417  pw2f1o2val  43455  wepwsolem  43458  fnwe2lem3  43468  lnmfg  43498  dgrsub2  43551  mpaaeu  43566  flcidc  43586  dflim5  43745  naddwordnexlem1  43813  rtrclexlem  44031  cnvrcl0  44040  brcoffn  44445  clsk1indlem3  44458  clsneif1o  44519  clsneicnv  44520  clsneikex  44521  clsneinex  44522  neicvgmex  44532  neicvgel1  44534  suprleubrd  44581  suprlubrd  44583  imo72b2  44587  dvconstbi  44749  bcc0  44755  binomcxplemnotnn0  44771  nnfoctb  45467  infleinflem1  45787  fprodcnlem  46017  sumnnodd  46048  icccncfext  46303  itgsin0pilem1  46366  stoweidlem32  46448  stoweidlem35  46451  stoweidlem36  46452  stoweidlem37  46453  stoweidlem43  46459  stoweidlem50  46466  wallispilem5  46485  stirlinglem2  46491  stirlinglem3  46492  stirlinglem4  46493  stirlinglem8  46497  stirlinglem11  46500  stirlinglem12  46501  stirlinglem14  46503  stirlinglem15  46504  fourierdlem11  46534  fourierdlem20  46543  fourierdlem21  46544  fourierdlem41  46564  fourierdlem42  46565  fourierdlem48  46570  fourierdlem49  46571  fourierdlem64  46586  fourierdlem71  46593  fourierdlem79  46601  fourierdlem90  46612  fourierdlem91  46613  fourierswlem  46646  etransclem17  46667  etransclem38  46688  saluni  46741  meaiininclem  46902  issmflelem  47160  issmfgtlem  47171  issmfgelem  47185  smflimsuplem4  47239  f1cof1blem  47510  zplusmodne  47785  m1modne  47790  submodneaddmod  47793  nndivides2  47820  sprval  47927  prprval  47962  bgoldbtbndlem2  48270  bgoldbtbndlem3  48271  bgoldbtbnd  48273  isubgrvtxuhgr  48328  isubgredg  48330  grimcnv  48352  isuspgrim  48360  gricushgr  48381  uhgrimisgrgric  48395  grtriclwlk3  48409  isubgr3stgrlem7  48436  grlimgrtri  48467  grlictr  48479  gpgvtx0  48517  gpgvtx1  48518  gpgprismgrusgra  48522  gpgedgvtx1  48526  gpg3kgrtriex  48553  pgnbgreunbgrlem3  48582  pgnbgreunbgrlem6  48588  isclintop  48671  clintopcllaw  48675  nzrneg1ne0  48694  lidldomn1  48695  zlidlring  48698  uzlidlring  48699  2zrngnmlid  48719  cznrng  48725  blenre  49038  blennn  49039  2arymaptf  49116  itcoval1  49127  itcovalendof  49133  ehl2eudisval0  49189  eenglngeehlnmlem2  49202  itsclc0yqsol  49228  inlinecirc02plem  49250  ipolub  49451  ipoglb  49454  nelsubclem  49530  imaid  49617  imaf1co  49618  uptri  49677  uptrar  49679  uptrai  49680  oppc1stflem  49750  setrec2mpt  50160