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  823  mpjaodan  961  mpjao3dan  1434  mpd3an3  1464  elabd2  3670  eueq2  3716  csbiegf  3932  difsnb  4806  reusv3i  5404  frpoinsg  6364  fimadmfo  6829  fimadmfoALT  6831  fvtresfn  7018  fvmpt3  7020  ffvelcdmd  7105  fnressn  7178  fsnex  7303  f1oiso2  7372  riota5f  7416  onsuc  7831  onsucuni  7848  frrlem10  8320  seqomlem2  8491  oaordi  8584  nnaordi  8656  qsdisj  8834  dom2lem  9032  canth2g  9171  limenpsi  9192  nnfi  9207  php4  9250  onfin  9267  sucxpdom  9291  xpfiOLD  9359  dmfi  9375  fiin  9462  supiso  9515  ordiso2  9555  wdom2d  9620  infeq5  9677  cantnfp1lem3  9720  cantnflem1d  9728  rankwflemb  9833  onenon  9989  cardonle  9997  sdomsdomcardi  10011  acni  10085  cardaleph  10129  djuen  10210  djuinf  10229  infdju1  10230  nnadju  10238  pwsdompw  10243  infdif  10248  cfval  10287  fin34  10430  fin1a2lem1  10440  fin1a2  10455  ttukeylem6  10554  sdomsdomcard  10600  canth3  10601  fpwwe2  10683  canthwelem  10690  gchdju1  10696  pwfseqlem4  10702  gchdjuidm  10708  gchxpidm  10709  tskwe2  10813  rankcf  10817  tskuni  10823  gruxp  10847  dmrecnq  11008  lterpq  11010  archnq  11020  reclem3pr  11089  reclem4pr  11090  0idsr  11137  lep1  12108  ledivp1  12170  negfi  12217  supaddc  12235  supmul1  12237  suprzcl  12698  uz11  12903  zmin  12986  zbtwnre  12988  rpnnen1lem4  13022  rpnnen1lem5  13023  xnegid  13280  supxrre  13369  infxrre  13378  eluzfz2  13572  fzsuc  13611  fzsuc2  13622  fzp1disj  13623  fzneuz  13648  nn0p1elfzo  13742  fllep1  13841  fraclt1  13842  fracle1  13843  fracge0  13844  flhalf  13870  ceige  13884  ceim1l  13887  fldiv  13900  modval  13911  suppssfz  14035  seqeq1  14045  expubnd  14217  iexpcyc  14246  binom2sub1  14260  faclbnd4lem3  14334  pfxid  14722  pfxccatpfx2  14775  swrdccat3blem  14777  cshw0  14832  cshwn  14835  cshimadifsn  14868  cshimadifsn0  14869  pfx2  14986  trclexlem  15033  shftfval  15109  shftcan1  15122  reval  15145  cjmulrcl  15183  addcj  15187  absval  15277  absneg  15316  abscj  15318  sqabsadd  15321  sqabssub  15322  leabs  15338  sqreulem  15398  lo1res  15595  o1of2  15649  o1rlimmul  15655  flo1  15890  trirecip  15899  efcan  16132  efi4p  16173  resin4p  16174  recos4p  16175  sincossq  16212  ruclem10  16275  iddvds  16307  1dvds  16308  2ebits  16484  lcmftp  16673  coprmgcdb  16686  1idssfct  16717  exprmfct  16741  eulerthlem2  16819  odzphi  16834  pcprendvds  16878  pcmpt  16930  oddprmdvds  16941  vdwlem8  17026  0ram2  17059  prmgaplem7  17095  setsn0fun  17210  setsexstruct2  17212  pwsvscaval  17540  2initoinv  18055  initoeu1  18056  initoeu2lem1  18059  initoeu2  18061  2termoinv  18062  termoeu1  18063  homarel  18081  joinfval  18418  meetfval  18432  latjcom  18492  latmcom  18508  0subm  18830  sgrp2nmndlem5  18942  grprcan  18991  isgrpid2  18994  grpinvid  19017  mulgnn0z  19119  0subgOLD  19170  qus0  19207  eqg0subg  19214  ghmker  19260  symgbasmap  19394  symginv  19420  pmtrfrn  19476  odmulg2  19573  slwpgp  19631  pj1eq  19718  efgtf  19740  frgpinv  19782  frgpup2  19794  cnaddablx  19886  cnaddabl  19887  zaddablx  19890  imasabl  19894  dprdfadd  20040  dpjidcl  20078  dpjlid  20081  pgpfac1lem3  20097  srgen1zr  20213  1unit  20374  unitgrpid  20385  1rinv  20395  irredn0  20423  irredneg  20430  c0snmgmhm  20462  rngisomring1  20468  zrrnghm  20536  rnrhmsubrg  20605  zrinitorngc  20642  zrtermorngc  20643  zrtermoringc  20675  isdrng2  20743  ringen1zr  20779  abv0  20824  abv1z  20825  abvneg  20827  lmodfopne  20898  lsssn0  20946  lspsn0  21006  lsp0  21007  lmhmvsca  21044  lmhmrnlss  21049  lmhmkerlss  21050  lsppratlem5  21153  rsp1  21247  kerlidl  21288  ring2idlqus  21319  rngqiprngfulem4  21324  rngqiprngfu  21327  cnfldneg  21408  zringcyg  21480  chrid  21540  chrrhm  21546  ip0r  21655  ocvlss  21690  ocv1  21697  rlmassa  21891  psrbagfsupp  21939  snifpsrbag  21940  psrbaglefi  21946  psrvscaval  21970  psrdi  21985  psrdir  21986  mplvscaval  22036  mhpmpl  22148  mhpdeg  22149  mhppwdeg  22154  psdmul  22170  psdpw  22174  coe1sclmulfv  22286  ply1idvr1OLD  22299  evl1var  22340  mamuvs1  22409  mamuvs2  22410  matecl  22431  matvscacell  22442  mat0scmat  22544  submaval0  22586  mdetrsca  22609  maduval  22644  minmar1val0  22653  pmatcollpw3fi1lem2  22793  chcoeffeqlem  22891  cayleyhamilton0  22895  cayleyhamiltonALT  22897  toponsspwpw  22928  cctop  23013  cldval  23031  ntrfval  23032  clsfval  23033  cmclsopn  23070  opncldf3  23094  neifval  23107  lpfval  23146  cnrmnrm  23369  dis2ndc  23468  islocfin  23525  tx1cn  23617  idqtop  23714  kqtopon  23735  kqid  23736  kqcld  23743  hmphen2  23807  filssufil  23920  ufileu  23927  alexsublem  24052  efmndtmd  24109  symgtgp  24114  ustuqtop4  24253  cstucnd  24293  metustexhalf  24569  nm0  24642  rlmnlm  24709  nmolb  24738  metdseq0  24876  pi1xfrval  25087  clmvneg1  25132  clmvsubval  25142  ipcau2  25268  tcphcphlem1  25269  tcphcphlem2  25270  cmetcaulem  25322  ovolicc2lem3  25554  ovolicc2lem4  25555  mbfmulc2lem  25682  i1fpos  25741  mbfi1fseqlem3  25752  itg2ge0  25770  bddiblnc  25877  dvres2  25947  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcobr  25983  dvcobrOLD  25984  dvfsumlem4  26070  ftc1a  26078  ftc1lem6  26082  uc1pmon1p  26191  ig1pval2  26216  dgradd2  26308  dgrcolem2  26314  plydivlem4  26338  plydiveu  26340  elqaalem3  26363  qaa  26365  ulmdvlem1  26443  abelthlem6  26480  abelthlem7  26482  eflogeq  26644  jensenlem2  27031  harmonicbnd4  27054  sgmnncl  27190  dchrptlem2  27309  1lgs  27384  lgs1  27385  2sqcoprm  27479  addsqnreup  27487  dchrisumlem2  27534  dchrisum0lem2a  27561  selberg2lem  27594  pntrsumo1  27609  pntrsumbnd  27610  pntpbnd1  27630  pntlemr  27646  pntlemj  27647  padicabvf  27675  bdayval  27693  noextendgt  27715  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetainflem4  27785  oldval  27893  divsmul  28245  divscl  28247  seqsp1  28317  zzs12  28423  remulscllem1  28432  incistruhgr  29096  subgrprop3  29293  subgruhgredgd  29301  usgrexi  29458  cusgrexi  29460  cusgrsizeinds  29470  vtxdgfusgrf  29515  1hevtxdg1  29524  1egrvtxdg1  29527  ewlkprop  29621  wlklenvm1  29640  wlkl1loop  29656  wlkp1lem4  29694  2pthnloop  29751  upgrclwlkcompim  29801  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0lem6  29835  crctcshwlkn0lem7  29836  crctcshlem4  29840  wspthnonp  29879  wlkswwlksf1o  29899  wwlksnwwlksnon  29935  umgr2wlkon  29970  wwlks2onv  29973  elwwlks2ons3im  29974  elwspths2spth  29987  umgrclwwlkge2  30010  clwlkclwwlkf1lem3  30025  erclwwlkref  30039  clwwlknp  30056  wwlksext2clwwlk  30076  wwlksubclwwlk  30077  0pthon1  30147  1wlkdlem4  30159  1pthd  30162  3spthd  30195  eupth2eucrct  30236  eucrctshift  30262  eucrct2eupth  30264  frgrncvvdeqlem8  30325  frgr2wwlkeqm  30350  isgrpoi  30517  grpoinvfval  30541  grpodivfval  30553  vcz  30594  cnaddabloOLD  30600  nvz0  30687  sspz  30754  lno0  30775  nmobndi  30794  ipasslem2  30851  shunssi  31387  ococin  31427  ssjo  31466  pjocini  31717  nlfnval  31900  lncnopbd  32056  riesz3i  32081  cnlnadjlem7  32092  pjclem4  32218  pj3si  32226  hstoc  32241  hstnmoc  32242  hstoh  32251  hst0  32252  mdsl2i  32341  chirredlem3  32411  chirredlem4  32412  dmdbr5ati  32441  rexunirn  32511  fcnvgreu  32683  infxrge0glb  32769  omndmul2  33089  omndmul  33091  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2lem7  33152  isarchi3  33194  orng0le1  33342  nsgqusf1olem2  33442  ssdifidllem  33484  ssmxidllem  33501  rprmdvdspow  33561  ressply1sub  33595  fedgmullem1  33680  extdg1id  33716  zartopn  33874  zarcmplem  33880  esumcvg  34087  esumcvgre  34092  sigaval  34112  unelldsys  34159  fiunelros  34175  measval  34199  pmeasmono  34326  probfinmeasb  34430  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemsi  34517  ballotlemfrci  34530  sgnneg  34543  signlem0  34602  breprexp  34648  bnj1006  34974  bnj1110  34996  bnj1253  35031  bnj1280  35034  bnj1463  35069  bnj1312  35072  erdszelem7  35202  erdszelem8  35203  cvmliftlem10  35299  cvmliftlem13  35301  cvmlift2lem9  35316  cvmlift3lem6  35329  cvmlift3lem7  35330  cvmlift3lem9  35332  satfv1lem  35367  dfrdg2  35796  cldregopn  36332  tailfval  36373  filnetlem3  36381  filnetlem4  36382  ontopbas  36429  bj-elid4  37169  bj-imdiridlem  37186  f1omptsnlem  37337  icoreunrn  37360  relowlpssretop  37365  fvineqsnf1  37411  wl-sbal2  37565  unccur  37610  poimirlem1  37628  poimirlem2  37629  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem11  37638  poimirlem12  37639  poimirlem17  37644  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem28  37655  poimir  37660  ismblfin  37668  cnambfre  37675  ftc1cnnc  37699  dvasin  37711  ismtyres  37815  heiborlem8  37825  ghomidOLD  37896  rngosn6  37933  rngonegmn1l  37948  rngonegmn1r  37949  rngoneglmul  37950  rngonegrmul  37951  idlnegcl  38029  0idl  38032  0rngo  38034  smprngopr  38059  cossex  38420  qsdisjALTV  38616  cnvepresdmqss  38653  mpets2  38842  lkrval  39089  ldualvaddval  39132  ldualvsval  39139  opoc1  39203  pmap0  39767  pmap1N  39769  pexmidALTN  39980  cdleme31fv  40392  cdlemg27b  40698  erngdvlem4  40993  erng0g  40996  erngdvlem4-rN  41001  dvalveclem  41027  dvh0g  41113  dih0cnv  41285  dih1rn  41289  dih1cnv  41290  doch0  41360  doch1  41361  lcfl7lem  41501  mapdheq  41730  hdmap1eq  41803  hdmapval2lem  41833  hgmapvvlem3  41927  zndvdchrrhm  41972  lcmineqlem13  42042  aks4d1p9  42089  primrootsunit1  42098  aks6d1c1p1  42108  aks6d1c1p6  42115  aks6d1c1p8  42116  sticksstones1  42147  sticksstones6  42152  sticksstones7  42153  sticksstones11  42157  sticksstones12a  42158  sticksstones12  42159  sticksstones22  42169  aks6d1c6isolem1  42175  aks6d1c6isolem2  42176  unitscyglem5  42200  renegid  42403  sn-0ne2  42436  remul01  42437  remulinvcom  42462  sn-0tie0  42469  renegmulnnass  42483  sn-inelr  42497  domnexpgn0cl  42533  abvexp  42542  frlmsnic  42550  fsuppssind  42603  mzpval  42743  mzpindd  42757  pellex  42846  2nn0ind  42957  jm2.26lem3  43013  pw2f1o2val  43051  wepwsolem  43054  fnwe2lem3  43064  lnmfg  43094  dgrsub2  43147  mpaaeu  43162  flcidc  43182  dflim5  43342  naddwordnexlem1  43410  rtrclexlem  43629  cnvrcl0  43638  brcoffn  44043  clsk1indlem3  44056  clsneif1o  44117  clsneicnv  44118  clsneikex  44119  clsneinex  44120  neicvgmex  44130  neicvgel1  44132  suprleubrd  44179  suprlubrd  44181  imo72b2  44185  dvconstbi  44353  bcc0  44359  binomcxplemnotnn0  44375  nnfoctb  45053  infleinflem1  45381  fprodcnlem  45614  sumnnodd  45645  icccncfext  45902  itgsin0pilem1  45965  stoweidlem32  46047  stoweidlem35  46050  stoweidlem36  46051  stoweidlem37  46052  stoweidlem43  46058  stoweidlem50  46065  wallispilem5  46084  stirlinglem2  46090  stirlinglem3  46091  stirlinglem4  46092  stirlinglem8  46096  stirlinglem11  46099  stirlinglem12  46100  stirlinglem14  46102  stirlinglem15  46103  fourierdlem11  46133  fourierdlem20  46142  fourierdlem21  46143  fourierdlem41  46163  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem64  46185  fourierdlem71  46192  fourierdlem79  46200  fourierdlem90  46211  fourierdlem91  46212  fourierswlem  46245  etransclem17  46266  etransclem38  46287  saluni  46340  meaiininclem  46501  issmflelem  46759  issmfgtlem  46770  issmfgelem  46784  smflimsuplem4  46838  f1cof1blem  47086  zplusmodne  47345  m1modne  47350  submodneaddmod  47353  sprval  47466  prprval  47501  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbnd  47796  isubgrvtxuhgr  47850  isubgredg  47852  isuspgrim  47875  grimcnv  47879  gricushgr  47886  uhgrimisgrgric  47899  grtriclwlk3  47912  isubgr3stgrlem7  47939  grlimgrtri  47963  grlictr  47975  gpgvtx0  48008  gpgvtx1  48009  gpgedgvtx1  48020  gpg3kgrtriex  48045  isclintop  48123  clintopcllaw  48127  nzrneg1ne0  48146  lidldomn1  48147  zlidlring  48150  uzlidlring  48151  2zrngnmlid  48171  cznrng  48177  coe1id  48301  blenre  48495  blennn  48496  2arymaptf  48573  itcoval1  48584  itcovalendof  48590  ehl2eudisval0  48646  eenglngeehlnmlem2  48659  itsclc0yqsol  48685  inlinecirc02plem  48707  ipolub  48877  ipoglb  48880  termcterm2  49146  setrec2mpt  49216