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  960  mpjao3dan  1431  mpd3an3  1461  elabd2  3669  eueq2  3718  csbiegf  3941  difsnb  4810  reusv3i  5409  frpoinsg  6365  fimadmfo  6829  fimadmfoALT  6831  fvtresfn  7017  fvmpt3  7019  ffvelcdmd  7104  fnressn  7177  fsnex  7302  f1oiso2  7371  riota5f  7415  onsuc  7830  onsucuni  7847  frrlem10  8318  seqomlem2  8489  oaordi  8582  nnaordi  8654  qsdisj  8832  dom2lem  9030  canth2g  9169  limenpsi  9190  nnfi  9205  php4  9247  onfin  9264  sucxpdom  9288  xpfiOLD  9356  dmfi  9372  fiin  9459  supiso  9512  ordiso2  9552  wdom2d  9617  infeq5  9674  cantnfp1lem3  9717  cantnflem1d  9725  rankwflemb  9830  onenon  9986  cardonle  9994  sdomsdomcardi  10008  acni  10082  cardaleph  10126  djuen  10207  djuinf  10226  infdju1  10227  nnadju  10235  pwsdompw  10240  infdif  10245  cfval  10284  fin34  10427  fin1a2lem1  10437  fin1a2  10452  ttukeylem6  10551  sdomsdomcard  10597  canth3  10598  fpwwe2  10680  canthwelem  10687  gchdju1  10693  pwfseqlem4  10699  gchdjuidm  10705  gchxpidm  10706  tskwe2  10810  rankcf  10814  tskuni  10820  gruxp  10844  dmrecnq  11005  lterpq  11007  archnq  11017  reclem3pr  11086  reclem4pr  11087  0idsr  11134  lep1  12105  ledivp1  12167  negfi  12214  supaddc  12232  supmul1  12234  suprzcl  12695  uz11  12900  zmin  12983  zbtwnre  12985  rpnnen1lem4  13019  rpnnen1lem5  13020  xnegid  13276  supxrre  13365  infxrre  13374  eluzfz2  13568  fzsuc  13607  fzsuc2  13618  fzp1disj  13619  fzneuz  13644  nn0p1elfzo  13738  fllep1  13837  fraclt1  13838  fracle1  13839  fracge0  13840  flhalf  13866  ceige  13880  ceim1l  13883  fldiv  13896  modval  13907  suppssfz  14031  seqeq1  14041  expubnd  14213  iexpcyc  14242  binom2sub1  14256  faclbnd4lem3  14330  pfxid  14718  pfxccatpfx2  14771  swrdccat3blem  14773  cshw0  14828  cshwn  14831  cshimadifsn  14864  cshimadifsn0  14865  pfx2  14982  trclexlem  15029  shftfval  15105  shftcan1  15118  reval  15141  cjmulrcl  15179  addcj  15183  absval  15273  absneg  15312  abscj  15314  sqabsadd  15317  sqabssub  15318  leabs  15334  sqreulem  15394  lo1res  15591  o1of2  15645  o1rlimmul  15651  flo1  15886  trirecip  15895  efcan  16128  efi4p  16169  resin4p  16170  recos4p  16171  sincossq  16208  ruclem10  16271  iddvds  16303  1dvds  16304  2ebits  16480  lcmftp  16669  coprmgcdb  16682  1idssfct  16713  exprmfct  16737  eulerthlem2  16815  odzphi  16829  pcprendvds  16873  pcmpt  16925  oddprmdvds  16936  vdwlem8  17021  0ram2  17054  prmgaplem7  17090  setsn0fun  17206  setsexstruct2  17208  pwsvscaval  17541  2initoinv  18063  initoeu1  18064  initoeu2lem1  18067  initoeu2  18069  2termoinv  18070  termoeu1  18071  homarel  18089  joinfval  18430  meetfval  18444  latjcom  18504  latmcom  18520  0subm  18842  sgrp2nmndlem5  18954  grprcan  19003  isgrpid2  19006  grpinvid  19029  mulgnn0z  19131  0subgOLD  19182  qus0  19219  eqg0subg  19226  ghmker  19272  symgbasmap  19408  symginv  19434  pmtrfrn  19490  odmulg2  19587  slwpgp  19645  pj1eq  19732  efgtf  19754  frgpinv  19796  frgpup2  19808  cnaddablx  19900  cnaddabl  19901  zaddablx  19904  imasabl  19908  dprdfadd  20054  dpjidcl  20092  dpjlid  20095  pgpfac1lem3  20111  srgen1zr  20233  1unit  20390  unitgrpid  20401  1rinv  20411  irredn0  20439  irredneg  20446  c0snmgmhm  20478  rngisomring1  20484  zrrnghm  20552  rnrhmsubrg  20621  zrinitorngc  20658  zrtermorngc  20659  zrtermoringc  20691  isdrng2  20759  ringen1zr  20795  abv0  20840  abv1z  20841  abvneg  20843  lmodfopne  20914  lsssn0  20963  lspsn0  21023  lsp0  21024  lmhmvsca  21061  lmhmrnlss  21066  lmhmkerlss  21067  lsppratlem5  21170  rsp1  21264  kerlidl  21305  ring2idlqus  21336  rngqiprngfulem4  21341  rngqiprngfu  21344  cnfldneg  21425  zringcyg  21497  chrid  21557  chrrhm  21563  ip0r  21672  ocvlss  21707  ocv1  21714  rlmassa  21908  psrbagfsupp  21956  snifpsrbag  21957  psrbaglefi  21963  psrvscaval  21987  psrdi  22002  psrdir  22003  mplvscaval  22053  mhpmpl  22165  mhpdeg  22166  mhppwdeg  22171  psdmul  22187  coe1sclmulfv  22301  ply1idvr1OLD  22314  evl1var  22355  mamuvs1  22424  mamuvs2  22425  matecl  22446  matvscacell  22457  mat0scmat  22559  submaval0  22601  mdetrsca  22624  maduval  22659  minmar1val0  22668  pmatcollpw3fi1lem2  22808  chcoeffeqlem  22906  cayleyhamilton0  22910  cayleyhamiltonALT  22912  toponsspwpw  22943  cctop  23028  cldval  23046  ntrfval  23047  clsfval  23048  cmclsopn  23085  opncldf3  23109  neifval  23122  lpfval  23161  cnrmnrm  23384  dis2ndc  23483  islocfin  23540  tx1cn  23632  idqtop  23729  kqtopon  23750  kqid  23751  kqcld  23758  hmphen2  23822  filssufil  23935  ufileu  23942  alexsublem  24067  efmndtmd  24124  symgtgp  24129  ustuqtop4  24268  cstucnd  24308  metustexhalf  24584  nm0  24657  rlmnlm  24724  nmolb  24753  metdseq0  24889  pi1xfrval  25100  clmvneg1  25145  clmvsubval  25155  ipcau2  25281  tcphcphlem1  25282  tcphcphlem2  25283  cmetcaulem  25335  ovolicc2lem3  25567  ovolicc2lem4  25568  mbfmulc2lem  25695  i1fpos  25755  mbfi1fseqlem3  25766  itg2ge0  25784  bddiblnc  25891  dvres2  25961  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcobr  25997  dvcobrOLD  25998  dvfsumlem4  26084  ftc1a  26092  ftc1lem6  26096  uc1pmon1p  26205  ig1pval2  26230  dgradd2  26322  dgrcolem2  26328  plydivlem4  26352  plydiveu  26354  elqaalem3  26377  qaa  26379  ulmdvlem1  26457  abelthlem6  26494  abelthlem7  26496  eflogeq  26658  jensenlem2  27045  harmonicbnd4  27068  sgmnncl  27204  dchrptlem2  27323  1lgs  27398  lgs1  27399  2sqcoprm  27493  addsqnreup  27501  dchrisumlem2  27548  dchrisum0lem2a  27575  selberg2lem  27608  pntrsumo1  27623  pntrsumbnd  27624  pntpbnd1  27644  pntlemr  27660  pntlemj  27661  padicabvf  27689  bdayval  27707  noextendgt  27729  nosupbnd2lem1  27774  noinfbnd2lem1  27789  noetainflem4  27799  oldval  27907  divsmul  28259  divscl  28261  seqsp1  28331  zzs12  28437  remulscllem1  28446  incistruhgr  29110  subgrprop3  29307  subgruhgredgd  29315  usgrexi  29472  cusgrexi  29474  cusgrsizeinds  29484  vtxdgfusgrf  29529  1hevtxdg1  29538  1egrvtxdg1  29541  ewlkprop  29635  wlklenvm1  29654  wlkl1loop  29670  wlkp1lem4  29708  2pthnloop  29763  upgrclwlkcompim  29813  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshwlkn0lem6  29844  crctcshwlkn0lem7  29845  crctcshlem4  29849  wspthnonp  29888  wlkswwlksf1o  29908  wwlksnwwlksnon  29944  umgr2wlkon  29979  wwlks2onv  29982  elwwlks2ons3im  29983  elwspths2spth  29996  umgrclwwlkge2  30019  clwlkclwwlkf1lem3  30034  erclwwlkref  30048  clwwlknp  30065  wwlksext2clwwlk  30085  wwlksubclwwlk  30086  0pthon1  30156  1wlkdlem4  30168  1pthd  30171  3spthd  30204  eupth2eucrct  30245  eucrctshift  30271  eucrct2eupth  30273  frgrncvvdeqlem8  30334  frgr2wwlkeqm  30359  isgrpoi  30526  grpoinvfval  30550  grpodivfval  30562  vcz  30603  cnaddabloOLD  30609  nvz0  30696  sspz  30763  lno0  30784  nmobndi  30803  ipasslem2  30860  shunssi  31396  ococin  31436  ssjo  31475  pjocini  31726  nlfnval  31909  lncnopbd  32065  riesz3i  32090  cnlnadjlem7  32101  pjclem4  32227  pj3si  32235  hstoc  32250  hstnmoc  32251  hstoh  32260  hst0  32261  mdsl2i  32350  chirredlem3  32420  chirredlem4  32421  dmdbr5ati  32450  rexunirn  32519  fcnvgreu  32689  infxrge0glb  32775  omndmul2  33071  omndmul  33073  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  isarchi3  33176  orng0le1  33321  nsgqusf1olem2  33421  ssdifidllem  33463  ssmxidllem  33480  rprmdvdspow  33540  ressply1sub  33574  fedgmullem1  33656  extdg1id  33690  zartopn  33835  zarcmplem  33841  esumcvg  34066  esumcvgre  34071  sigaval  34091  unelldsys  34138  fiunelros  34154  measval  34178  pmeasmono  34305  probfinmeasb  34409  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemsi  34495  ballotlemfrci  34508  sgnneg  34521  signlem0  34580  breprexp  34626  bnj1006  34952  bnj1110  34974  bnj1253  35009  bnj1280  35012  bnj1463  35047  bnj1312  35050  erdszelem7  35181  erdszelem8  35182  cvmliftlem10  35278  cvmliftlem13  35280  cvmlift2lem9  35295  cvmlift3lem6  35308  cvmlift3lem7  35309  cvmlift3lem9  35311  satfv1lem  35346  dfrdg2  35776  cldregopn  36313  tailfval  36354  filnetlem3  36362  filnetlem4  36363  ontopbas  36410  bj-elid4  37150  bj-imdiridlem  37167  f1omptsnlem  37318  icoreunrn  37341  relowlpssretop  37346  fvineqsnf1  37392  wl-sbal2  37544  unccur  37589  poimirlem1  37607  poimirlem2  37608  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem11  37617  poimirlem12  37618  poimirlem17  37623  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem28  37634  poimir  37639  ismblfin  37647  cnambfre  37654  ftc1cnnc  37678  dvasin  37690  ismtyres  37794  heiborlem8  37804  ghomidOLD  37875  rngosn6  37912  rngonegmn1l  37927  rngonegmn1r  37928  rngoneglmul  37929  rngonegrmul  37930  idlnegcl  38008  0idl  38011  0rngo  38013  smprngopr  38038  cossex  38400  qsdisjALTV  38596  cnvepresdmqss  38633  mpets2  38822  lkrval  39069  ldualvaddval  39112  ldualvsval  39119  opoc1  39183  pmap0  39747  pmap1N  39749  pexmidALTN  39960  cdleme31fv  40372  cdlemg27b  40678  erngdvlem4  40973  erng0g  40976  erngdvlem4-rN  40981  dvalveclem  41007  dvh0g  41093  dih0cnv  41265  dih1rn  41269  dih1cnv  41270  doch0  41340  doch1  41341  lcfl7lem  41481  mapdheq  41710  hdmap1eq  41783  hdmapval2lem  41813  hgmapvvlem3  41907  zndvdchrrhm  41952  lcmineqlem13  42022  aks4d1p9  42069  primrootsunit1  42078  aks6d1c1p1  42088  aks6d1c1p6  42095  aks6d1c1p8  42096  sticksstones1  42127  sticksstones6  42132  sticksstones7  42133  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  unitscyglem5  42180  renegid  42379  sn-0ne2  42412  remul01  42413  remulinvcom  42438  sn-0tie0  42445  renegmulnnass  42459  sn-inelr  42473  domnexpgn0cl  42509  abvexp  42518  frlmsnic  42526  fsuppssind  42579  mzpval  42719  mzpindd  42733  pellex  42822  2nn0ind  42933  jm2.26lem3  42989  pw2f1o2val  43027  wepwsolem  43030  fnwe2lem3  43040  lnmfg  43070  dgrsub2  43123  mpaaeu  43138  flcidc  43158  dflim5  43318  naddwordnexlem1  43386  rtrclexlem  43605  cnvrcl0  43614  brcoffn  44019  clsk1indlem3  44032  clsneif1o  44093  clsneicnv  44094  clsneikex  44095  clsneinex  44096  neicvgmex  44106  neicvgel1  44108  suprleubrd  44155  suprlubrd  44157  imo72b2  44161  dvconstbi  44329  bcc0  44335  binomcxplemnotnn0  44351  nnfoctb  44986  infleinflem1  45319  fprodcnlem  45554  sumnnodd  45585  icccncfext  45842  itgsin0pilem1  45905  stoweidlem32  45987  stoweidlem35  45990  stoweidlem36  45991  stoweidlem37  45992  stoweidlem43  45998  stoweidlem50  46005  wallispilem5  46024  stirlinglem2  46030  stirlinglem3  46031  stirlinglem4  46032  stirlinglem8  46036  stirlinglem11  46039  stirlinglem12  46040  stirlinglem14  46042  stirlinglem15  46043  fourierdlem11  46073  fourierdlem20  46082  fourierdlem21  46083  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem64  46125  fourierdlem71  46132  fourierdlem79  46140  fourierdlem90  46151  fourierdlem91  46152  fourierswlem  46185  etransclem17  46206  etransclem38  46227  saluni  46280  meaiininclem  46441  issmflelem  46699  issmfgtlem  46710  issmfgelem  46724  smflimsuplem4  46778  f1cof1blem  47023  zplusmodne  47282  m1modne  47287  submodneaddmod  47290  sprval  47403  prprval  47438  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbnd  47733  isubgrvtxuhgr  47787  isubgredg  47789  isuspgrim  47812  grimcnv  47816  gricushgr  47823  uhgrimisgrgric  47836  grtriclwlk3  47849  isubgr3stgrlem7  47874  grlimgrtri  47898  grlictr  47910  gpgvtx0  47943  gpgvtx1  47944  gpgedgvtx1  47954  isclintop  48050  clintopcllaw  48054  nzrneg1ne0  48073  lidldomn1  48074  zlidlring  48077  uzlidlring  48078  2zrngnmlid  48098  cznrng  48104  coe1id  48229  blenre  48423  blennn  48424  2arymaptf  48501  itcoval1  48512  itcovalendof  48518  ehl2eudisval0  48574  eenglngeehlnmlem2  48587  itsclc0yqsol  48613  inlinecirc02plem  48635  ipolub  48776  ipoglb  48779  setrec2mpt  48927