Theorem mpdan 687

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 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  689  mpan2  691  biadanid  822  mpjaodan  960  mpjao3dan  1434  mpd3an3  1464  elabd2  3639  eueq2  3684  csbiegf  3898  difsnb  4773  reusv3i  5362  frpoinsg  6319  fimadmfo  6784  fimadmfoALT  6786  fvtresfn  6973  fvmpt3  6975  ffvelcdmd  7060  fnressn  7133  fsnex  7261  f1oiso2  7330  riota5f  7375  onsuc  7790  onsucuni  7806  frrlem10  8277  seqomlem2  8422  oaordi  8513  nnaordi  8585  qsdisj  8770  dom2lem  8966  canth2g  9101  limenpsi  9122  nnfi  9137  php4  9180  onfin  9185  sucxpdom  9209  xpfiOLD  9277  dmfi  9293  fiin  9380  supiso  9434  ordiso2  9475  wdom2d  9540  infeq5  9597  cantnfp1lem3  9640  cantnflem1d  9648  rankwflemb  9753  onenon  9909  cardonle  9917  sdomsdomcardi  9931  acni  10005  cardaleph  10049  djuen  10130  djuinf  10149  infdju1  10150  nnadju  10158  pwsdompw  10163  infdif  10168  cfval  10207  fin34  10350  fin1a2lem1  10360  fin1a2  10375  ttukeylem6  10474  sdomsdomcard  10520  canth3  10521  fpwwe2  10603  canthwelem  10610  gchdju1  10616  pwfseqlem4  10622  gchdjuidm  10628  gchxpidm  10629  tskwe2  10733  rankcf  10737  tskuni  10743  gruxp  10767  dmrecnq  10928  lterpq  10930  archnq  10940  reclem3pr  11009  reclem4pr  11010  0idsr  11057  lep1  12030  ledivp1  12092  negfi  12139  supaddc  12157  supmul1  12159  suprzcl  12621  uz11  12825  zmin  12910  zbtwnre  12912  rpnnen1lem4  12946  rpnnen1lem5  12947  xnegid  13205  supxrre  13294  infxrre  13304  eluzfz2  13500  fzsuc  13539  fzsuc2  13550  fzp1disj  13551  fzneuz  13576  nn0p1elfzo  13670  fllep1  13770  fraclt1  13771  fracle1  13772  fracge0  13773  flhalf  13799  ceige  13813  ceim1l  13816  fldiv  13829  modval  13840  suppssfz  13966  seqeq1  13976  expubnd  14150  iexpcyc  14179  binom2sub1  14193  faclbnd4lem3  14267  pfxid  14656  pfxccatpfx2  14709  swrdccat3blem  14711  cshw0  14766  cshwn  14769  cshimadifsn  14802  cshimadifsn0  14803  pfx2  14920  trclexlem  14967  shftfval  15043  shftcan1  15056  reval  15079  cjmulrcl  15117  addcj  15121  absval  15211  absneg  15250  abscj  15252  sqabsadd  15255  sqabssub  15256  leabs  15272  sqreulem  15333  lo1res  15532  o1of2  15586  o1rlimmul  15592  flo1  15827  trirecip  15836  efcan  16069  efi4p  16112  resin4p  16113  recos4p  16114  sincossq  16151  ruclem10  16214  iddvds  16246  1dvds  16247  2ebits  16424  lcmftp  16613  coprmgcdb  16626  1idssfct  16657  exprmfct  16681  eulerthlem2  16759  odzphi  16774  pcprendvds  16818  pcmpt  16870  oddprmdvds  16881  vdwlem8  16966  0ram2  16999  prmgaplem7  17035  setsn0fun  17150  setsexstruct2  17152  pwsvscaval  17465  2initoinv  17979  initoeu1  17980  initoeu2lem1  17983  initoeu2  17985  2termoinv  17986  termoeu1  17987  homarel  18005  joinfval  18339  meetfval  18353  latjcom  18413  latmcom  18429  0subm  18751  sgrp2nmndlem5  18863  grprcan  18912  isgrpid2  18915  grpinvid  18938  mulgnn0z  19040  0subgOLD  19091  qus0  19128  eqg0subg  19135  ghmker  19181  symgbasmap  19314  symginv  19339  pmtrfrn  19395  odmulg2  19492  slwpgp  19550  pj1eq  19637  efgtf  19659  frgpinv  19701  frgpup2  19713  cnaddablx  19805  cnaddabl  19806  zaddablx  19809  imasabl  19813  dprdfadd  19959  dpjidcl  19997  dpjlid  20000  pgpfac1lem3  20016  srgen1zr  20132  1unit  20290  unitgrpid  20301  1rinv  20311  irredn0  20339  irredneg  20346  c0snmgmhm  20378  rngisomring1  20384  zrrnghm  20452  rnrhmsubrg  20521  zrinitorngc  20558  zrtermorngc  20559  zrtermoringc  20591  isdrng2  20659  ringen1zr  20694  abv0  20739  abv1z  20740  abvneg  20742  lmodfopne  20813  lsssn0  20861  lspsn0  20921  lsp0  20922  lmhmvsca  20959  lmhmrnlss  20964  lmhmkerlss  20965  lsppratlem5  21068  rsp1  21154  kerlidl  21195  ring2idlqus  21226  rngqiprngfulem4  21231  rngqiprngfu  21234  cnfldneg  21314  zringcyg  21386  chrid  21442  chrrhm  21448  ip0r  21553  ocvlss  21588  ocv1  21595  rlmassa  21787  psrbagfsupp  21835  snifpsrbag  21836  psrbaglefi  21842  psrvscaval  21866  psrdi  21881  psrdir  21882  mplvscaval  21932  mhpmpl  22038  mhpdeg  22039  mhppwdeg  22044  psdmul  22060  psdpw  22064  coe1sclmulfv  22176  ply1idvr1OLD  22189  evl1var  22230  mamuvs1  22299  mamuvs2  22300  matecl  22319  matvscacell  22330  mat0scmat  22432  submaval0  22474  mdetrsca  22497  maduval  22532  minmar1val0  22541  pmatcollpw3fi1lem2  22681  chcoeffeqlem  22779  cayleyhamilton0  22783  cayleyhamiltonALT  22785  toponsspwpw  22816  cctop  22900  cldval  22917  ntrfval  22918  clsfval  22919  cmclsopn  22956  opncldf3  22980  neifval  22993  lpfval  23032  cnrmnrm  23255  dis2ndc  23354  islocfin  23411  tx1cn  23503  idqtop  23600  kqtopon  23621  kqid  23622  kqcld  23629  hmphen2  23693  filssufil  23806  ufileu  23813  alexsublem  23938  efmndtmd  23995  symgtgp  24000  ustuqtop4  24139  cstucnd  24178  metustexhalf  24451  nm0  24524  rlmnlm  24583  nmolb  24612  metdseq0  24750  pi1xfrval  24961  clmvneg1  25006  clmvsubval  25016  ipcau2  25141  tcphcphlem1  25142  tcphcphlem2  25143  cmetcaulem  25195  ovolicc2lem3  25427  ovolicc2lem4  25428  mbfmulc2lem  25555  i1fpos  25614  mbfi1fseqlem3  25625  itg2ge0  25643  bddiblnc  25750  dvres2  25820  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcobr  25856  dvcobrOLD  25857  dvfsumlem4  25943  ftc1a  25951  ftc1lem6  25955  uc1pmon1p  26064  ig1pval2  26089  dgradd2  26181  dgrcolem2  26187  plydivlem4  26211  plydiveu  26213  elqaalem3  26236  qaa  26238  ulmdvlem1  26316  abelthlem6  26353  abelthlem7  26355  eflogeq  26518  jensenlem2  26905  harmonicbnd4  26928  sgmnncl  27064  dchrptlem2  27183  1lgs  27258  lgs1  27259  2sqcoprm  27353  addsqnreup  27361  dchrisumlem2  27408  dchrisum0lem2a  27435  selberg2lem  27468  pntrsumo1  27483  pntrsumbnd  27484  pntpbnd1  27504  pntlemr  27520  pntlemj  27521  padicabvf  27549  bdayval  27567  noextendgt  27589  nosupbnd2lem1  27634  noinfbnd2lem1  27649  noetainflem4  27659  oldval  27769  divsmul  28130  divscl  28132  seqsp1  28212  zzs12  28346  remulscllem1  28358  incistruhgr  29013  subgrprop3  29210  subgruhgredgd  29218  usgrexi  29375  cusgrexi  29377  cusgrsizeinds  29387  vtxdgfusgrf  29432  1hevtxdg1  29441  1egrvtxdg1  29444  ewlkprop  29538  wlklenvm1  29557  wlkl1loop  29573  wlkp1lem4  29611  2pthnloop  29668  upgrclwlkcompim  29718  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  crctcshwlkn0lem6  29752  crctcshwlkn0lem7  29753  crctcshlem4  29757  wspthnonp  29796  wlkswwlksf1o  29816  wwlksnwwlksnon  29852  umgr2wlkon  29887  wwlks2onv  29890  elwwlks2ons3im  29891  elwspths2spth  29904  umgrclwwlkge2  29927  clwlkclwwlkf1lem3  29942  erclwwlkref  29956  clwwlknp  29973  wwlksext2clwwlk  29993  wwlksubclwwlk  29994  0pthon1  30064  1wlkdlem4  30076  1pthd  30079  3spthd  30112  eupth2eucrct  30153  eucrctshift  30179  eucrct2eupth  30181  frgrncvvdeqlem8  30242  frgr2wwlkeqm  30267  isgrpoi  30434  grpoinvfval  30458  grpodivfval  30470  vcz  30511  cnaddabloOLD  30517  nvz0  30604  sspz  30671  lno0  30692  nmobndi  30711  ipasslem2  30768  shunssi  31304  ococin  31344  ssjo  31383  pjocini  31634  nlfnval  31817  lncnopbd  31973  riesz3i  31998  cnlnadjlem7  32009  pjclem4  32135  pj3si  32143  hstoc  32158  hstnmoc  32159  hstoh  32168  hst0  32169  mdsl2i  32258  chirredlem3  32328  chirredlem4  32329  dmdbr5ati  32358  rexunirn  32428  fcnvgreu  32604  infxrge0glb  32695  sgnneg  32765  omndmul2  33033  omndmul  33035  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  isarchi3  33148  orng0le1  33297  nsgqusf1olem2  33392  ssdifidllem  33434  ssmxidllem  33451  rprmdvdspow  33511  ressply1sub  33546  fedgmullem1  33632  extdg1id  33668  nn0constr  33758  zartopn  33872  zarcmplem  33878  esumcvg  34083  esumcvgre  34088  sigaval  34108  unelldsys  34155  fiunelros  34171  measval  34195  pmeasmono  34322  probfinmeasb  34426  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemsi  34513  ballotlemfrci  34526  signlem0  34585  breprexp  34631  bnj1006  34957  bnj1110  34979  bnj1253  35014  bnj1280  35017  bnj1463  35052  bnj1312  35055  erdszelem7  35191  erdszelem8  35192  cvmliftlem10  35288  cvmliftlem13  35290  cvmlift2lem9  35305  cvmlift3lem6  35318  cvmlift3lem7  35319  cvmlift3lem9  35321  satfv1lem  35356  dfrdg2  35790  cldregopn  36326  tailfval  36367  filnetlem3  36375  filnetlem4  36376  ontopbas  36423  bj-elid4  37163  bj-imdiridlem  37180  f1omptsnlem  37331  icoreunrn  37354  relowlpssretop  37359  fvineqsnf1  37405  wl-sbal2  37559  unccur  37604  poimirlem1  37622  poimirlem2  37623  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem11  37632  poimirlem12  37633  poimirlem17  37638  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem28  37649  poimir  37654  ismblfin  37662  cnambfre  37669  ftc1cnnc  37693  dvasin  37705  ismtyres  37809  heiborlem8  37819  ghomidOLD  37890  rngosn6  37927  rngonegmn1l  37942  rngonegmn1r  37943  rngoneglmul  37944  rngonegrmul  37945  idlnegcl  38023  0idl  38026  0rngo  38028  smprngopr  38053  cossex  38417  qsdisjALTV  38613  cnvepresdmqss  38651  mpets2  38840  lkrval  39088  ldualvaddval  39131  ldualvsval  39138  opoc1  39202  pmap0  39766  pmap1N  39768  pexmidALTN  39979  cdleme31fv  40391  cdlemg27b  40697  erngdvlem4  40992  erng0g  40995  erngdvlem4-rN  41000  dvalveclem  41026  dvh0g  41112  dih0cnv  41284  dih1rn  41288  dih1cnv  41289  doch0  41359  doch1  41360  lcfl7lem  41500  mapdheq  41729  hdmap1eq  41802  hdmapval2lem  41832  hgmapvvlem3  41926  zndvdchrrhm  41967  lcmineqlem13  42036  aks4d1p9  42083  primrootsunit1  42092  aks6d1c1p1  42102  aks6d1c1p6  42109  aks6d1c1p8  42110  sticksstones1  42141  sticksstones6  42146  sticksstones7  42147  sticksstones11  42151  sticksstones12a  42152  sticksstones12  42153  sticksstones22  42163  aks6d1c6isolem1  42169  aks6d1c6isolem2  42170  unitscyglem5  42194  renegid  42368  sn-0ne2  42401  remul01  42402  remulinvcom  42428  sn-0tie0  42446  renegmulnnass  42460  domnexpgn0cl  42518  abvexp  42527  frlmsnic  42535  fsuppssind  42588  mzpval  42727  mzpindd  42741  pellex  42830  2nn0ind  42941  jm2.26lem3  42997  pw2f1o2val  43035  wepwsolem  43038  fnwe2lem3  43048  lnmfg  43078  dgrsub2  43131  mpaaeu  43146  flcidc  43166  dflim5  43325  naddwordnexlem1  43393  rtrclexlem  43612  cnvrcl0  43621  brcoffn  44026  clsk1indlem3  44039  clsneif1o  44100  clsneicnv  44101  clsneikex  44102  clsneinex  44103  neicvgmex  44113  neicvgel1  44115  suprleubrd  44162  suprlubrd  44164  imo72b2  44168  dvconstbi  44330  bcc0  44336  binomcxplemnotnn0  44352  nnfoctb  45049  infleinflem1  45373  fprodcnlem  45604  sumnnodd  45635  icccncfext  45892  itgsin0pilem1  45955  stoweidlem32  46037  stoweidlem35  46040  stoweidlem36  46041  stoweidlem37  46042  stoweidlem43  46048  stoweidlem50  46055  wallispilem5  46074  stirlinglem2  46080  stirlinglem3  46081  stirlinglem4  46082  stirlinglem8  46086  stirlinglem11  46089  stirlinglem12  46090  stirlinglem14  46092  stirlinglem15  46093  fourierdlem11  46123  fourierdlem20  46132  fourierdlem21  46133  fourierdlem41  46153  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem64  46175  fourierdlem71  46182  fourierdlem79  46190  fourierdlem90  46201  fourierdlem91  46202  fourierswlem  46235  etransclem17  46256  etransclem38  46277  saluni  46330  meaiininclem  46491  issmflelem  46749  issmfgtlem  46760  issmfgelem  46774  smflimsuplem4  46828  f1cof1blem  47079  zplusmodne  47348  m1modne  47353  submodneaddmod  47356  sprval  47484  prprval  47519  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbnd  47814  isubgrvtxuhgr  47868  isubgredg  47870  grimcnv  47892  isuspgrim  47900  gricushgr  47921  uhgrimisgrgric  47935  grtriclwlk3  47948  isubgr3stgrlem7  47975  grlimgrtri  47999  grlictr  48011  gpgvtx0  48048  gpgvtx1  48049  gpgprismgrusgra  48053  gpgedgvtx1  48057  gpg3kgrtriex  48084  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  isclintop  48199  clintopcllaw  48203  nzrneg1ne0  48222  lidldomn1  48223  zlidlring  48226  uzlidlring  48227  2zrngnmlid  48247  cznrng  48253  coe1id  48377  blenre  48567  blennn  48568  2arymaptf  48645  itcoval1  48656  itcovalendof  48662  ehl2eudisval0  48718  eenglngeehlnmlem2  48731  itsclc0yqsol  48757  inlinecirc02plem  48779  ipolub  48980  ipoglb  48983  nelsubclem  49060  imaid  49147  imaf1co  49148  uptri  49207  uptrar  49209  uptrai  49210  oppc1stflem  49280  setrec2mpt  49690