Theorem mpdan 670

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 575	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  mpidan  672  mpan2  674  mpjaodan  972  mpd3an3  1579  eueq2  3578  csbiegf  3752  difsnb  4527  reusv3i  5073  fvtresfn  6505  fvmpt3  6507  ffvelrnd  6582  fnressn  6649  fsnex  6762  f1oiso2  6826  riota5f  6860  onsucuni  7258  wfrlem5  7655  seqomlem2  7782  oaordi  7863  nnaordi  7935  qsdisj  8059  dom2lem  8232  canth2g  8353  limenpsi  8374  php4  8386  onfin  8390  sucxpdom  8408  xpfi  8470  dmfi  8483  pwfilem  8499  pwfi  8500  fiin  8567  supiso  8620  ordiso2  8659  wdom2d  8724  infeq5  8781  cantnfp1lem3  8824  cantnflem1d  8832  rankwflemb  8903  onenon  9058  cardonle  9066  sdomsdomcardi  9080  acni  9151  cardaleph  9195  cdaen  9280  cdainf  9299  infcda1  9300  pwsdompw  9311  infdif  9316  cfval  9354  fin34  9497  fin1a2lem1  9507  fin1a2  9522  ttukeylem6  9621  sdomsdomcard  9667  canth3  9668  fpwwe2  9750  canthwelem  9757  gchcda1  9763  pwfseqlem4  9769  gchcdaidm  9775  gchxpidm  9776  tskwe2  9880  rankcf  9884  tskuni  9890  gruxp  9914  dmrecnq  10075  lterpq  10077  archnq  10087  reclem3pr  10156  reclem4pr  10157  0idsr  10203  lep1  11147  ledivp1  11210  negfi  11256  supaddc  11275  supmul1  11277  suprzcl  11723  uz11  11927  zmin  12003  zbtwnre  12005  rpnnen1lem4  12036  rpnnen1lem5  12037  xnegid  12287  xrsupss  12357  xrinfmss  12358  supxrre  12375  infxrre  12384  eluzfz2  12572  fzsuc  12611  fzsuc2  12621  fzp1disj  12622  fzneuz  12644  nn0p1elfzo  12735  fllep1  12826  fraclt1  12827  fracle1  12828  fracge0  12829  flhalf  12855  ceige  12868  ceim1l  12870  fldiv  12883  modval  12894  suppssfz  13017  seqeq1  13027  expubnd  13144  iexpcyc  13192  binom2sub1  13205  faclbnd4lem3  13302  swrdid  13652  swrdccat3blem  13719  cshwn  13767  cshimadifsn  13799  cshimadifsn0  13800  trclexlem  13958  shftfval  14033  shftcan1  14046  reval  14069  cjmulrcl  14107  addcj  14111  absval  14201  absneg  14240  abscj  14242  sqabsadd  14245  sqabssub  14246  leabs  14262  sqreulem  14322  lo1res  14513  o1of2  14566  o1rlimmul  14572  flo1  14808  trirecip  14817  efcan  15046  efi4p  15087  resin4p  15088  recos4p  15089  sincossq  15126  ruclem10  15188  iddvds  15218  1dvds  15219  2ebits  15388  lcmftp  15568  coprmgcdb  15581  1idssfct  15611  exprmfct  15633  eulerthlem2  15704  odzphi  15718  pcprendvds  15762  pcmpt  15813  vdwlem8  15909  0ram2  15942  prmgaplem7  15978  setsn0fun  16106  setsexstruct2  16108  pwsvscaval  16360  issect2  16618  2initoinv  16864  initoeu1  16865  initoeu2lem1  16868  initoeu2  16870  2termoinv  16871  termoeu1  16872  homarel  16890  joinfval  17206  meetfval  17220  latjcom  17264  latmcom  17280  sgrp2nmndlem5  17621  grprcan  17660  isgrpid2  17663  grpinvid  17681  mulgnn0z  17771  0subg  17821  qus0  17854  ghmker  17888  symginv  18023  pmtrfrn  18079  odmulg2  18173  slwpgp  18229  pj1eq  18314  efgtf  18336  frgpinv  18378  frgpup2  18390  mulgnn0di  18432  cnaddablx  18472  cnaddabl  18473  zaddablx  18476  dprdfadd  18621  dpjidcl  18659  dpjlid  18662  pgpfac1lem3  18678  srgen1zr  18732  ringlz  18789  ringrz  18790  1unit  18860  unitgrpid  18871  1rinv  18881  irredn0  18905  irredneg  18912  isdrng2  18961  abv0  19035  abv1z  19036  abvneg  19038  lmodfopne  19105  lsssn0  19152  lspsn0  19215  lsp0  19216  lmhmvsca  19252  lmhmrnlss  19257  lmhmkerlss  19258  lsppratlem5  19360  rsp1  19433  ringen1zr  19486  rlmassa  19535  snifpsrbag  19575  psrvscaval  19601  psrdi  19615  psrdir  19616  mplsubglem  19643  mplvscaval  19657  coe1sclmulfv  19861  ply1idvr1  19871  evl1var  19908  cnfldneg  19980  zringcyg  20047  chrid  20083  chrrhm  20087  ip0r  20192  ocvlss  20226  ocv1  20233  mamuvs1  20421  mamuvs2  20422  matecl  20441  matvscacell  20452  mat0scmat  20555  submaval0  20597  mdetrsca  20620  maduval  20655  minmar1val0  20664  pmatcollpw3fi1lem2  20805  chfacfscmulgsum  20878  chfacfpmmulgsum  20882  chcoeffeqlem  20903  cayleyhamilton0  20907  cayleyhamiltonALT  20909  toponsspwpw  20940  cctop  21024  cldval  21041  ntrfval  21042  clsfval  21043  cmclsopn  21080  opncldf3  21104  neifval  21117  lpfval  21156  cnrmnrm  21379  islocfin  21534  tx1cn  21626  idqtop  21723  kqtopon  21744  kqid  21745  kqcld  21752  hmphen2  21816  filssufil  21929  ufileu  21936  alexsublem  22061  symgtgp  22118  ustuqtop4  22261  cstucnd  22301  metustexhalf  22574  nm0  22646  rlmnlm  22705  nmolb  22734  metdseq0  22870  pi1xfrval  23066  clmvneg1  23111  clmvsubval  23121  ipcau2  23245  tchcphlem1  23246  tchcphlem2  23247  cmetcaulem  23298  ovolicc2lem3  23500  ovolicc2lem4  23501  mbfmulc2lem  23628  i1fpos  23687  mbfi1fseqlem3  23698  mbfi1fseqlem4  23699  itg2ge0  23716  dvres2  23890  dvaddbr  23915  dvmulbr  23916  dvcobr  23923  dvfsumlem4  24006  ftc1a  24014  ftc1lem6  24018  uc1pmon1p  24125  ig1pval2  24147  dgradd2  24238  dgrcolem2  24244  plydivlem4  24265  plydiveu  24267  elqaalem3  24290  qaa  24292  ulmdvlem1  24368  abelthlem6  24404  abelthlem7  24406  eflogeq  24562  jensenlem2  24928  harmonicbnd4  24951  sgmnncl  25087  dchrptlem2  25204  1lgs  25279  lgs1  25280  dchrisumlem2  25393  dchrisum0lem2a  25420  selberg2lem  25453  pntrsumo1  25468  pntrsumbnd  25469  pntpbnd1  25489  pntlemr  25505  pntlemj  25506  padicabvf  25534  istrkg3ld  25574  incistruhgr  26188  subgrprop3  26384  subgruhgredgd  26392  usgrexi  26565  cusgrexi  26567  cusgrsizeinds  26576  vtxdgfusgrf  26621  1hevtxdg1  26630  1egrvtxdg1  26633  ewlkprop  26727  wlklenvm1  26745  wlkl1loop  26762  wlkp1lem4  26801  2pthnloop  26855  upgrclwlkcompim  26905  crctcshwlkn0lem4  26934  crctcshwlkn0lem5  26935  crctcshwlkn0lem6  26936  crctcshwlkn0lem7  26937  crctcshlem4  26941  wspthnonp  26986  wlkswwlksf1o  27006  wwlksnwwlksnon  27053  wwlksnwwlksnonOLD  27055  umgr2wlkon  27090  wwlks2onv  27093  elwwlks2ons3im  27094  elwwlks2ons3OLD  27096  elwspths2spth  27109  umgrclwwlkge2  27134  clwlkclwwlkf1lem3  27149  erclwwlkref  27163  clwwlknp  27185  wwlksext2clwwlk  27207  wwlksubclwwlk  27209  0pthon1  27301  1wlkdlem4  27313  1pthd  27316  3spthd  27349  eupth2eucrct  27390  eucrctshift  27416  eucrct2eupth  27418  frgrncvvdeqlem8  27481  frgr2wwlkeqm  27506  isgrpoi  27681  grpoinvfval  27705  grpodivfval  27717  vcz  27758  cnaddabloOLD  27764  nvz0  27851  sspz  27918  lno0  27939  nmobndi  27958  ipasslem2  28015  shunssi  28555  ococin  28595  ssjo  28634  pjocini  28885  nlfnval  29068  lncnopbd  29224  riesz3i  29249  cnlnadjlem7  29260  pjclem4  29386  pj3si  29394  hstoc  29409  hstnmoc  29410  hstoh  29419  hst0  29420  mdsl2i  29509  chirredlem3  29579  chirredlem4  29580  dmdbr5ati  29609  rexunirn  29657  fcnvgreu  29799  infxrge0glb  29857  2sqcoprm  29972  omndmul2  30037  omndmul  30039  isarchi3  30066  orng0le1  30137  esumcvg  30473  esumcvgre  30478  sigaval  30498  unelldsys  30546  fiunelros  30562  measval  30586  pmeasmono  30711  eulerpartlemgvv  30763  probfinmeasb  30816  ballotlemfc0  30879  ballotlemfcc  30880  ballotlemsi  30901  ballotlemfrci  30914  sgnneg  30927  signlem0  30989  breprexp  31036  bnj1006  31352  bnj1110  31373  bnj1253  31408  bnj1280  31411  bnj1463  31446  bnj1312  31449  erdszelem7  31502  erdszelem8  31503  cvmliftlem10  31599  cvmliftlem13  31601  cvmlift2lem9  31616  cvmlift3lem6  31629  cvmlift3lem7  31630  cvmlift3lem9  31632  dfrdg2  32021  dftrpred3g  32053  frpoinsg  32062  frrlem5  32105  bdayval  32122  noextendgt  32144  nosupbnd2lem1  32182  cldregopn  32647  tailfval  32688  filnetlem3  32696  filnetlem4  32697  ontopbas  32744  f1omptsnlem  33500  icoreunrn  33523  relowlpssretop  33528  wl-sbal2  33661  unccur  33705  poimirlem1  33723  poimirlem2  33724  poimirlem4  33726  poimirlem6  33728  poimirlem7  33729  poimirlem11  33733  poimirlem12  33734  poimirlem17  33739  poimirlem20  33742  poimirlem22  33744  poimirlem23  33745  poimirlem28  33750  poimir  33755  ismblfin  33763  cnambfre  33770  bddiblnc  33792  ftc1cnnc  33796  dvasin  33808  ismtyres  33918  heiborlem8  33928  ghomidOLD  33999  rngolz  34032  rngorz  34033  rngosn6  34036  rngonegmn1l  34051  rngonegmn1r  34052  rngoneglmul  34053  rngonegrmul  34054  idlnegcl  34132  0idl  34135  0rngo  34137  keridl  34142  smprngopr  34162  cossex  34487  lkrval  34868  ldualvaddval  34911  ldualvsval  34918  opoc1  34982  pmap0  35545  pmap1N  35547  pexmidALTN  35758  cdleme31fv  36171  cdlemg27b  36477  erngdvlem4  36772  erng0g  36775  erngdvlem4-rN  36780  dvalveclem  36806  dvh0g  36892  dih0cnv  37064  dih1rn  37068  dih1cnv  37069  doch0  37139  doch1  37140  lcfl7lem  37280  mapdheq  37509  hdmap1eq  37582  hdmapval2lem  37612  hgmapvvlem3  37706  mzpval  37797  mzpindd  37811  pellex  37901  2nn0ind  38011  jm2.26lem3  38069  pw2f1o2val  38107  wepwsolem  38113  fnwe2lem3  38123  lnmfg  38153  dgrsub2  38206  mpaaeu  38221  flcidc  38245  rtrclexlem  38423  cnvrcl0  38432  brcoffn  38828  clsk1indlem3  38841  clsneif1o  38902  clsneicnv  38903  clsneikex  38904  clsneinex  38905  neicvgmex  38915  neicvgel1  38917  suprleubrd  38966  suprlubrd  38970  imo72b2  38975  dvconstbi  39033  bcc0  39039  binomcxplemnotnn0  39055  nnfoctb  39706  infleinflem1  40066  fprodcnlem  40311  sumnnodd  40342  icccncfext  40580  itgsin0pilem1  40645  stoweidlem22  40718  stoweidlem32  40728  stoweidlem35  40731  stoweidlem36  40732  stoweidlem37  40733  stoweidlem43  40739  stoweidlem50  40746  wallispilem5  40765  stirlinglem2  40771  stirlinglem3  40772  stirlinglem4  40773  stirlinglem8  40777  stirlinglem11  40780  stirlinglem12  40781  stirlinglem14  40783  stirlinglem15  40784  fourierdlem11  40814  fourierdlem20  40823  fourierdlem21  40824  fourierdlem41  40844  fourierdlem42  40845  fourierdlem48  40850  fourierdlem49  40851  fourierdlem64  40866  fourierdlem71  40873  fourierdlem79  40881  fourierdlem90  40892  fourierdlem91  40893  fourierswlem  40926  etransclem17  40947  etransclem38  40968  saluni  41023  meaiininclem  41182  issmflelem  41435  issmfgtlem  41446  issmfgelem  41459  smflimsuplem4  41511  pfxid  41967  pfx2  41987  bgoldbtbndlem2  42269  bgoldbtbndlem3  42270  bgoldbtbnd  42272  sprval  42297  isclintop  42411  clintopcllaw  42415  nzrneg1ne0  42437  rnglz  42452  c0snmgmhm  42482  zrrnghm  42485  lidldomn1  42489  zlidlring  42496  uzlidlring  42497  2zrngnmlid  42517  cznrng  42523  zrinitorngc  42568  zrtermorngc  42569  zrtermoringc  42638  coe1id  42740  blenre  42936  blennn  42937  onsetreclem2  43020