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  3683  csbiegf  3897  difsnb  4772  reusv3i  5361  frpoinsg  6318  fimadmfo  6783  fimadmfoALT  6785  fvtresfn  6972  fvmpt3  6974  ffvelcdmd  7059  fnressn  7132  fsnex  7260  f1oiso2  7329  riota5f  7374  onsuc  7789  onsucuni  7805  frrlem10  8276  seqomlem2  8421  oaordi  8512  nnaordi  8584  qsdisj  8769  dom2lem  8965  canth2g  9100  limenpsi  9121  nnfi  9136  php4  9179  onfin  9184  sucxpdom  9208  xpfiOLD  9276  dmfi  9292  fiin  9379  supiso  9433  ordiso2  9474  wdom2d  9539  infeq5  9596  cantnfp1lem3  9639  cantnflem1d  9647  rankwflemb  9752  onenon  9908  cardonle  9916  sdomsdomcardi  9930  acni  10004  cardaleph  10048  djuen  10129  djuinf  10148  infdju1  10149  nnadju  10157  pwsdompw  10162  infdif  10167  cfval  10206  fin34  10349  fin1a2lem1  10359  fin1a2  10374  ttukeylem6  10473  sdomsdomcard  10519  canth3  10520  fpwwe2  10602  canthwelem  10609  gchdju1  10615  pwfseqlem4  10621  gchdjuidm  10627  gchxpidm  10628  tskwe2  10732  rankcf  10736  tskuni  10742  gruxp  10766  dmrecnq  10927  lterpq  10929  archnq  10939  reclem3pr  11008  reclem4pr  11009  0idsr  11056  lep1  12029  ledivp1  12091  negfi  12138  supaddc  12156  supmul1  12158  suprzcl  12620  uz11  12824  zmin  12909  zbtwnre  12911  rpnnen1lem4  12945  rpnnen1lem5  12946  xnegid  13204  supxrre  13293  infxrre  13303  eluzfz2  13499  fzsuc  13538  fzsuc2  13549  fzp1disj  13550  fzneuz  13575  nn0p1elfzo  13669  fllep1  13769  fraclt1  13770  fracle1  13771  fracge0  13772  flhalf  13798  ceige  13812  ceim1l  13815  fldiv  13828  modval  13839  suppssfz  13965  seqeq1  13975  expubnd  14149  iexpcyc  14178  binom2sub1  14192  faclbnd4lem3  14266  pfxid  14655  pfxccatpfx2  14708  swrdccat3blem  14710  cshw0  14765  cshwn  14768  cshimadifsn  14801  cshimadifsn0  14802  pfx2  14919  trclexlem  14966  shftfval  15042  shftcan1  15055  reval  15078  cjmulrcl  15116  addcj  15120  absval  15210  absneg  15249  abscj  15251  sqabsadd  15254  sqabssub  15255  leabs  15271  sqreulem  15332  lo1res  15531  o1of2  15585  o1rlimmul  15591  flo1  15826  trirecip  15835  efcan  16068  efi4p  16111  resin4p  16112  recos4p  16113  sincossq  16150  ruclem10  16213  iddvds  16245  1dvds  16246  2ebits  16423  lcmftp  16612  coprmgcdb  16625  1idssfct  16656  exprmfct  16680  eulerthlem2  16758  odzphi  16773  pcprendvds  16817  pcmpt  16869  oddprmdvds  16880  vdwlem8  16965  0ram2  16998  prmgaplem7  17034  setsn0fun  17149  setsexstruct2  17151  pwsvscaval  17464  2initoinv  17978  initoeu1  17979  initoeu2lem1  17982  initoeu2  17984  2termoinv  17985  termoeu1  17986  homarel  18004  joinfval  18338  meetfval  18352  latjcom  18412  latmcom  18428  0subm  18750  sgrp2nmndlem5  18862  grprcan  18911  isgrpid2  18914  grpinvid  18937  mulgnn0z  19039  0subgOLD  19090  qus0  19127  eqg0subg  19134  ghmker  19180  symgbasmap  19313  symginv  19338  pmtrfrn  19394  odmulg2  19491  slwpgp  19549  pj1eq  19636  efgtf  19658  frgpinv  19700  frgpup2  19712  cnaddablx  19804  cnaddabl  19805  zaddablx  19808  imasabl  19812  dprdfadd  19958  dpjidcl  19996  dpjlid  19999  pgpfac1lem3  20015  srgen1zr  20131  1unit  20289  unitgrpid  20300  1rinv  20310  irredn0  20338  irredneg  20345  c0snmgmhm  20377  rngisomring1  20383  zrrnghm  20451  rnrhmsubrg  20520  zrinitorngc  20557  zrtermorngc  20558  zrtermoringc  20590  isdrng2  20658  ringen1zr  20693  abv0  20738  abv1z  20739  abvneg  20741  lmodfopne  20812  lsssn0  20860  lspsn0  20920  lsp0  20921  lmhmvsca  20958  lmhmrnlss  20963  lmhmkerlss  20964  lsppratlem5  21067  rsp1  21153  kerlidl  21194  ring2idlqus  21225  rngqiprngfulem4  21230  rngqiprngfu  21233  cnfldneg  21313  zringcyg  21385  chrid  21441  chrrhm  21447  ip0r  21552  ocvlss  21587  ocv1  21594  rlmassa  21786  psrbagfsupp  21834  snifpsrbag  21835  psrbaglefi  21841  psrvscaval  21865  psrdi  21880  psrdir  21881  mplvscaval  21931  mhpmpl  22037  mhpdeg  22038  mhppwdeg  22043  psdmul  22059  psdpw  22063  coe1sclmulfv  22175  ply1idvr1OLD  22188  evl1var  22229  mamuvs1  22298  mamuvs2  22299  matecl  22318  matvscacell  22329  mat0scmat  22431  submaval0  22473  mdetrsca  22496  maduval  22531  minmar1val0  22540  pmatcollpw3fi1lem2  22680  chcoeffeqlem  22778  cayleyhamilton0  22782  cayleyhamiltonALT  22784  toponsspwpw  22815  cctop  22899  cldval  22916  ntrfval  22917  clsfval  22918  cmclsopn  22955  opncldf3  22979  neifval  22992  lpfval  23031  cnrmnrm  23254  dis2ndc  23353  islocfin  23410  tx1cn  23502  idqtop  23599  kqtopon  23620  kqid  23621  kqcld  23628  hmphen2  23692  filssufil  23805  ufileu  23812  alexsublem  23937  efmndtmd  23994  symgtgp  23999  ustuqtop4  24138  cstucnd  24177  metustexhalf  24450  nm0  24523  rlmnlm  24582  nmolb  24611  metdseq0  24749  pi1xfrval  24960  clmvneg1  25005  clmvsubval  25015  ipcau2  25140  tcphcphlem1  25141  tcphcphlem2  25142  cmetcaulem  25194  ovolicc2lem3  25426  ovolicc2lem4  25427  mbfmulc2lem  25554  i1fpos  25613  mbfi1fseqlem3  25624  itg2ge0  25642  bddiblnc  25749  dvres2  25819  dvaddbr  25846  dvmulbr  25847  dvmulbrOLD  25848  dvcobr  25855  dvcobrOLD  25856  dvfsumlem4  25942  ftc1a  25950  ftc1lem6  25954  uc1pmon1p  26063  ig1pval2  26088  dgradd2  26180  dgrcolem2  26186  plydivlem4  26210  plydiveu  26212  elqaalem3  26235  qaa  26237  ulmdvlem1  26315  abelthlem6  26352  abelthlem7  26354  eflogeq  26517  jensenlem2  26904  harmonicbnd4  26927  sgmnncl  27063  dchrptlem2  27182  1lgs  27257  lgs1  27258  2sqcoprm  27352  addsqnreup  27360  dchrisumlem2  27407  dchrisum0lem2a  27434  selberg2lem  27467  pntrsumo1  27482  pntrsumbnd  27483  pntpbnd1  27503  pntlemr  27519  pntlemj  27520  padicabvf  27548  bdayval  27566  noextendgt  27588  nosupbnd2lem1  27633  noinfbnd2lem1  27648  noetainflem4  27658  oldval  27768  divsmul  28129  divscl  28131  seqsp1  28211  zzs12  28345  remulscllem1  28357  incistruhgr  29012  subgrprop3  29209  subgruhgredgd  29217  usgrexi  29374  cusgrexi  29376  cusgrsizeinds  29386  vtxdgfusgrf  29431  1hevtxdg1  29440  1egrvtxdg1  29443  ewlkprop  29537  wlklenvm1  29556  wlkl1loop  29572  wlkp1lem4  29610  2pthnloop  29667  upgrclwlkcompim  29717  crctcshwlkn0lem4  29749  crctcshwlkn0lem5  29750  crctcshwlkn0lem6  29751  crctcshwlkn0lem7  29752  crctcshlem4  29756  wspthnonp  29795  wlkswwlksf1o  29815  wwlksnwwlksnon  29851  umgr2wlkon  29886  wwlks2onv  29889  elwwlks2ons3im  29890  elwspths2spth  29903  umgrclwwlkge2  29926  clwlkclwwlkf1lem3  29941  erclwwlkref  29955  clwwlknp  29972  wwlksext2clwwlk  29992  wwlksubclwwlk  29993  0pthon1  30063  1wlkdlem4  30075  1pthd  30078  3spthd  30111  eupth2eucrct  30152  eucrctshift  30178  eucrct2eupth  30180  frgrncvvdeqlem8  30241  frgr2wwlkeqm  30266  isgrpoi  30433  grpoinvfval  30457  grpodivfval  30469  vcz  30510  cnaddabloOLD  30516  nvz0  30603  sspz  30670  lno0  30691  nmobndi  30710  ipasslem2  30767  shunssi  31303  ococin  31343  ssjo  31382  pjocini  31633  nlfnval  31816  lncnopbd  31972  riesz3i  31997  cnlnadjlem7  32008  pjclem4  32134  pj3si  32142  hstoc  32157  hstnmoc  32158  hstoh  32167  hst0  32168  mdsl2i  32257  chirredlem3  32327  chirredlem4  32328  dmdbr5ati  32357  rexunirn  32427  fcnvgreu  32603  infxrge0glb  32694  sgnneg  32764  omndmul2  33032  omndmul  33034  cycpmco2lem5  33093  cycpmco2lem6  33094  cycpmco2lem7  33095  isarchi3  33147  orng0le1  33296  nsgqusf1olem2  33391  ssdifidllem  33433  ssmxidllem  33450  rprmdvdspow  33510  ressply1sub  33545  fedgmullem1  33631  extdg1id  33667  nn0constr  33757  zartopn  33871  zarcmplem  33877  esumcvg  34082  esumcvgre  34087  sigaval  34107  unelldsys  34154  fiunelros  34170  measval  34194  pmeasmono  34321  probfinmeasb  34425  ballotlemfc0  34490  ballotlemfcc  34491  ballotlemsi  34512  ballotlemfrci  34525  signlem0  34584  breprexp  34630  bnj1006  34956  bnj1110  34978  bnj1253  35013  bnj1280  35016  bnj1463  35051  bnj1312  35054  erdszelem7  35184  erdszelem8  35185  cvmliftlem10  35281  cvmliftlem13  35283  cvmlift2lem9  35298  cvmlift3lem6  35311  cvmlift3lem7  35312  cvmlift3lem9  35314  satfv1lem  35349  dfrdg2  35778  cldregopn  36314  tailfval  36355  filnetlem3  36363  filnetlem4  36364  ontopbas  36411  bj-elid4  37151  bj-imdiridlem  37168  f1omptsnlem  37319  icoreunrn  37342  relowlpssretop  37347  fvineqsnf1  37393  wl-sbal2  37547  unccur  37592  poimirlem1  37610  poimirlem2  37611  poimirlem4  37613  poimirlem6  37615  poimirlem7  37616  poimirlem11  37620  poimirlem12  37621  poimirlem17  37626  poimirlem20  37629  poimirlem22  37631  poimirlem23  37632  poimirlem28  37637  poimir  37642  ismblfin  37650  cnambfre  37657  ftc1cnnc  37681  dvasin  37693  ismtyres  37797  heiborlem8  37807  ghomidOLD  37878  rngosn6  37915  rngonegmn1l  37930  rngonegmn1r  37931  rngoneglmul  37932  rngonegrmul  37933  idlnegcl  38011  0idl  38014  0rngo  38016  smprngopr  38041  cossex  38405  qsdisjALTV  38601  cnvepresdmqss  38639  mpets2  38828  lkrval  39076  ldualvaddval  39119  ldualvsval  39126  opoc1  39190  pmap0  39754  pmap1N  39756  pexmidALTN  39967  cdleme31fv  40379  cdlemg27b  40685  erngdvlem4  40980  erng0g  40983  erngdvlem4-rN  40988  dvalveclem  41014  dvh0g  41100  dih0cnv  41272  dih1rn  41276  dih1cnv  41277  doch0  41347  doch1  41348  lcfl7lem  41488  mapdheq  41717  hdmap1eq  41790  hdmapval2lem  41820  hgmapvvlem3  41914  zndvdchrrhm  41955  lcmineqlem13  42024  aks4d1p9  42071  primrootsunit1  42080  aks6d1c1p1  42090  aks6d1c1p6  42097  aks6d1c1p8  42098  sticksstones1  42129  sticksstones6  42134  sticksstones7  42135  sticksstones11  42139  sticksstones12a  42140  sticksstones12  42141  sticksstones22  42151  aks6d1c6isolem1  42157  aks6d1c6isolem2  42158  unitscyglem5  42182  renegid  42356  sn-0ne2  42389  remul01  42390  remulinvcom  42416  sn-0tie0  42434  renegmulnnass  42448  sn-inelr  42468  domnexpgn0cl  42504  abvexp  42513  frlmsnic  42521  fsuppssind  42574  mzpval  42713  mzpindd  42727  pellex  42816  2nn0ind  42927  jm2.26lem3  42983  pw2f1o2val  43021  wepwsolem  43024  fnwe2lem3  43034  lnmfg  43064  dgrsub2  43117  mpaaeu  43132  flcidc  43152  dflim5  43311  naddwordnexlem1  43379  rtrclexlem  43598  cnvrcl0  43607  brcoffn  44012  clsk1indlem3  44025  clsneif1o  44086  clsneicnv  44087  clsneikex  44088  clsneinex  44089  neicvgmex  44099  neicvgel1  44101  suprleubrd  44148  suprlubrd  44150  imo72b2  44154  dvconstbi  44316  bcc0  44322  binomcxplemnotnn0  44338  nnfoctb  45035  infleinflem1  45359  fprodcnlem  45590  sumnnodd  45621  icccncfext  45878  itgsin0pilem1  45941  stoweidlem32  46023  stoweidlem35  46026  stoweidlem36  46027  stoweidlem37  46028  stoweidlem43  46034  stoweidlem50  46041  wallispilem5  46060  stirlinglem2  46066  stirlinglem3  46067  stirlinglem4  46068  stirlinglem8  46072  stirlinglem11  46075  stirlinglem12  46076  stirlinglem14  46078  stirlinglem15  46079  fourierdlem11  46109  fourierdlem20  46118  fourierdlem21  46119  fourierdlem41  46139  fourierdlem42  46140  fourierdlem48  46145  fourierdlem49  46146  fourierdlem64  46161  fourierdlem71  46168  fourierdlem79  46176  fourierdlem90  46187  fourierdlem91  46188  fourierswlem  46221  etransclem17  46242  etransclem38  46263  saluni  46316  meaiininclem  46477  issmflelem  46735  issmfgtlem  46746  issmfgelem  46760  smflimsuplem4  46814  f1cof1blem  47065  zplusmodne  47334  m1modne  47339  submodneaddmod  47342  sprval  47470  prprval  47505  bgoldbtbndlem2  47797  bgoldbtbndlem3  47798  bgoldbtbnd  47800  isubgrvtxuhgr  47854  isubgredg  47856  grimcnv  47878  isuspgrim  47886  gricushgr  47907  uhgrimisgrgric  47921  grtriclwlk3  47934  isubgr3stgrlem7  47961  grlimgrtri  47985  grlictr  47997  gpgvtx0  48034  gpgvtx1  48035  gpgprismgrusgra  48039  gpgedgvtx1  48043  gpg3kgrtriex  48070  pgnbgreunbgrlem3  48098  pgnbgreunbgrlem6  48104  isclintop  48185  clintopcllaw  48189  nzrneg1ne0  48208  lidldomn1  48209  zlidlring  48212  uzlidlring  48213  2zrngnmlid  48233  cznrng  48239  coe1id  48363  blenre  48553  blennn  48554  2arymaptf  48631  itcoval1  48642  itcovalendof  48648  ehl2eudisval0  48704  eenglngeehlnmlem2  48717  itsclc0yqsol  48743  inlinecirc02plem  48765  ipolub  48966  ipoglb  48969  nelsubclem  49046  imaid  49133  imaf1co  49134  uptri  49193  uptrar  49195  uptrai  49196  oppc1stflem  49266  setrec2mpt  49676