Theorem mpdan 686

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  mpidan  688  mpan2  690  mpjaodan  956  mpjao3dan  1428  mpd3an3  1459  eueq2  3649  csbiegf  3861  difsnb  4699  reusv3i  5270  fimadmfo  6574  fimadmfoALT  6576  fvtresfn  6747  fvmpt3  6749  ffvelrnd  6829  fnressn  6897  fsnex  7017  f1oiso2  7084  riota5f  7121  onsucuni  7523  seqomlem2  8070  oaordi  8155  nnaordi  8227  qsdisj  8357  dom2lem  8532  canth2g  8655  limenpsi  8676  php4  8688  onfin  8694  sucxpdom  8711  xpfi  8773  dmfi  8786  pwfilem  8802  pwfi  8803  fiin  8870  supiso  8923  ordiso2  8963  wdom2d  9028  infeq5  9084  cantnfp1lem3  9127  cantnflem1d  9135  rankwflemb  9206  onenon  9362  cardonle  9370  sdomsdomcardi  9384  acni  9456  cardaleph  9500  djuen  9580  djuinf  9599  infdju1  9600  nnadju  9608  pwsdompw  9615  infdif  9620  cfval  9658  fin34  9801  fin1a2lem1  9811  fin1a2  9826  ttukeylem6  9925  sdomsdomcard  9971  canth3  9972  fpwwe2  10054  canthwelem  10061  gchdju1  10067  pwfseqlem4  10073  gchdjuidm  10079  gchxpidm  10080  tskwe2  10184  rankcf  10188  tskuni  10194  gruxp  10218  dmrecnq  10379  lterpq  10381  archnq  10391  reclem3pr  10460  reclem4pr  10461  0idsr  10508  lep1  11470  ledivp1  11531  negfi  11577  supaddc  11595  supmul1  11597  suprzcl  12050  uz11  12255  zmin  12332  zbtwnre  12334  rpnnen1lem4  12367  rpnnen1lem5  12368  xnegid  12619  supxrre  12708  infxrre  12717  eluzfz2  12910  fzsuc  12949  fzsuc2  12960  fzp1disj  12961  fzneuz  12983  nn0p1elfzo  13075  fllep1  13166  fraclt1  13167  fracle1  13168  fracge0  13169  flhalf  13195  ceige  13208  ceim1l  13210  fldiv  13223  modval  13234  suppssfz  13357  seqeq1  13367  expubnd  13537  iexpcyc  13565  binom2sub1  13578  faclbnd4lem3  13651  pfxid  14037  pfxccatpfx2  14090  swrdccat3blem  14092  cshw0  14147  cshwn  14150  cshimadifsn  14182  cshimadifsn0  14183  pfx2  14300  trclexlem  14345  shftfval  14421  shftcan1  14434  reval  14457  cjmulrcl  14495  addcj  14499  absval  14589  absneg  14629  abscj  14631  sqabsadd  14634  sqabssub  14635  leabs  14651  sqreulem  14711  lo1res  14908  o1of2  14961  o1rlimmul  14967  flo1  15201  trirecip  15210  efcan  15441  efi4p  15482  resin4p  15483  recos4p  15484  sincossq  15521  ruclem10  15584  iddvds  15615  1dvds  15616  2ebits  15786  lcmftp  15970  coprmgcdb  15983  1idssfct  16014  exprmfct  16038  eulerthlem2  16109  odzphi  16123  pcprendvds  16167  pcmpt  16218  oddprmdvds  16229  vdwlem8  16314  0ram2  16347  prmgaplem7  16383  setsn0fun  16512  setsexstruct2  16514  pwsvscaval  16760  2initoinv  17262  initoeu1  17263  initoeu2lem1  17266  initoeu2  17268  2termoinv  17269  termoeu1  17270  homarel  17288  joinfval  17603  meetfval  17617  latjcom  17661  latmcom  17677  0subm  17974  sgrp2nmndlem5  18086  grprcan  18129  isgrpid2  18132  grpinvid  18152  mulgnn0z  18246  0subg  18296  qus0  18330  ghmker  18376  symgbasmap  18497  symginv  18522  pmtrfrn  18578  odmulg2  18674  slwpgp  18730  pj1eq  18818  efgtf  18840  frgpinv  18882  frgpup2  18894  cnaddablx  18981  cnaddabl  18982  zaddablx  18985  dprdfadd  19135  dpjidcl  19173  dpjlid  19176  pgpfac1lem3  19192  srgen1zr  19273  1unit  19404  unitgrpid  19415  1rinv  19425  irredn0  19449  irredneg  19456  isdrng2  19505  rnrhmsubrg  19560  abv0  19595  abv1z  19596  abvneg  19598  lmodfopne  19665  lsssn0  19712  lspsn0  19773  lsp0  19774  lmhmvsca  19810  lmhmrnlss  19815  lmhmkerlss  19816  lsppratlem5  19916  rsp1  19990  ringen1zr  20043  cnfldneg  20117  zringcyg  20184  chrid  20219  chrrhm  20223  ip0r  20326  ocvlss  20361  ocv1  20368  rlmassa  20557  snifpsrbag  20604  psrvscaval  20630  psrdi  20644  psrdir  20645  mplvscaval  20687  mhpmpl  20795  mhpdeg  20796  coe1sclmulfv  20912  ply1idvr1  20922  evl1var  20960  mamuvs1  21010  mamuvs2  21011  matecl  21030  matvscacell  21041  mat0scmat  21143  submaval0  21185  mdetrsca  21208  maduval  21243  minmar1val0  21252  pmatcollpw3fi1lem2  21392  chcoeffeqlem  21490  cayleyhamilton0  21494  cayleyhamiltonALT  21496  toponsspwpw  21527  cctop  21611  cldval  21628  ntrfval  21629  clsfval  21630  cmclsopn  21667  opncldf3  21691  neifval  21704  lpfval  21743  cnrmnrm  21966  dis2ndc  22065  islocfin  22122  tx1cn  22214  idqtop  22311  kqtopon  22332  kqid  22333  kqcld  22340  hmphen2  22404  filssufil  22517  ufileu  22524  alexsublem  22649  efmndtmd  22706  symgtgp  22711  ustuqtop4  22850  cstucnd  22890  metustexhalf  23163  nm0  23235  rlmnlm  23294  nmolb  23323  metdseq0  23459  pi1xfrval  23659  clmvneg1  23704  clmvsubval  23714  ipcau2  23838  tcphcphlem1  23839  tcphcphlem2  23840  cmetcaulem  23892  ovolicc2lem3  24123  ovolicc2lem4  24124  mbfmulc2lem  24251  i1fpos  24310  mbfi1fseqlem3  24321  itg2ge0  24339  bddiblnc  24445  dvres2  24515  dvaddbr  24541  dvmulbr  24542  dvcobr  24549  dvfsumlem4  24632  ftc1a  24640  ftc1lem6  24644  uc1pmon1p  24752  ig1pval2  24774  dgradd2  24865  dgrcolem2  24871  plydivlem4  24892  plydiveu  24894  elqaalem3  24917  qaa  24919  ulmdvlem1  24995  abelthlem6  25031  abelthlem7  25033  eflogeq  25193  jensenlem2  25573  harmonicbnd4  25596  sgmnncl  25732  dchrptlem2  25849  1lgs  25924  lgs1  25925  2sqcoprm  26019  addsqnreup  26027  dchrisumlem2  26074  dchrisum0lem2a  26101  selberg2lem  26134  pntrsumo1  26149  pntrsumbnd  26150  pntpbnd1  26170  pntlemr  26186  pntlemj  26187  padicabvf  26215  incistruhgr  26872  subgrprop3  27066  subgruhgredgd  27074  usgrexi  27231  cusgrexi  27233  cusgrsizeinds  27242  vtxdgfusgrf  27287  1hevtxdg1  27296  1egrvtxdg1  27299  ewlkprop  27393  wlklenvm1  27411  wlkl1loop  27427  wlkp1lem4  27466  2pthnloop  27520  upgrclwlkcompim  27570  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  crctcshwlkn0lem6  27601  crctcshwlkn0lem7  27602  crctcshlem4  27606  wspthnonp  27645  wlkswwlksf1o  27665  wwlksnwwlksnon  27701  umgr2wlkon  27736  wwlks2onv  27739  elwwlks2ons3im  27740  elwspths2spth  27753  umgrclwwlkge2  27776  clwlkclwwlkf1lem3  27791  erclwwlkref  27805  clwwlknp  27822  wwlksext2clwwlk  27842  wwlksubclwwlk  27843  0pthon1  27913  1wlkdlem4  27925  1pthd  27928  3spthd  27961  eupth2eucrct  28002  eucrctshift  28028  eucrct2eupth  28030  frgrncvvdeqlem8  28091  frgr2wwlkeqm  28116  isgrpoi  28281  grpoinvfval  28305  grpodivfval  28317  vcz  28358  cnaddabloOLD  28364  nvz0  28451  sspz  28518  lno0  28539  nmobndi  28558  ipasslem2  28615  shunssi  29151  ococin  29191  ssjo  29230  pjocini  29481  nlfnval  29664  lncnopbd  29820  riesz3i  29845  cnlnadjlem7  29856  pjclem4  29982  pj3si  29990  hstoc  30005  hstnmoc  30006  hstoh  30015  hst0  30016  mdsl2i  30105  chirredlem3  30175  chirredlem4  30176  dmdbr5ati  30205  biadanid  30236  rexunirn  30263  fcnvgreu  30436  infxrge0glb  30515  omndmul2  30763  omndmul  30765  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2lem7  30824  isarchi3  30866  orng0le1  30936  kerlidl  31012  ssmxidllem  31049  fedgmullem1  31113  extdg1id  31141  zartopn  31228  zarcmplem  31234  esumcvg  31455  esumcvgre  31460  sigaval  31480  unelldsys  31527  fiunelros  31543  measval  31567  pmeasmono  31692  probfinmeasb  31796  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemsi  31882  ballotlemfrci  31895  sgnneg  31908  signlem0  31967  breprexp  32014  bnj1006  32342  bnj1110  32364  bnj1253  32399  bnj1280  32402  bnj1463  32437  bnj1312  32440  erdszelem7  32557  erdszelem8  32558  cvmliftlem10  32654  cvmliftlem13  32656  cvmlift2lem9  32671  cvmlift3lem6  32684  cvmlift3lem7  32685  cvmlift3lem9  32687  satfv1lem  32722  dfrdg2  33153  dftrpred3g  33185  frpoinsg  33194  frrlem10  33245  bdayval  33268  noextendgt  33290  nosupbnd2lem1  33328  cldregopn  33792  tailfval  33833  filnetlem3  33841  filnetlem4  33842  ontopbas  33889  bj-elid4  34583  bj-imdiridlem  34600  f1omptsnlem  34753  icoreunrn  34776  relowlpssretop  34781  fvineqsnf1  34827  wl-sbal2  34965  unccur  35040  poimirlem1  35058  poimirlem2  35059  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem11  35068  poimirlem12  35069  poimirlem17  35074  poimirlem20  35077  poimirlem22  35079  poimirlem23  35080  poimirlem28  35085  poimir  35090  ismblfin  35098  cnambfre  35105  ftc1cnnc  35129  dvasin  35141  ismtyres  35246  heiborlem8  35256  ghomidOLD  35327  rngosn6  35364  rngonegmn1l  35379  rngonegmn1r  35380  rngoneglmul  35381  rngonegrmul  35382  idlnegcl  35460  0idl  35463  0rngo  35465  smprngopr  35490  cossex  35824  qsdisjALTV  36010  cnvepresdmqss  36046  lkrval  36384  ldualvaddval  36427  ldualvsval  36434  opoc1  36498  pmap0  37061  pmap1N  37063  pexmidALTN  37274  cdleme31fv  37686  cdlemg27b  37992  erngdvlem4  38287  erng0g  38290  erngdvlem4-rN  38295  dvalveclem  38321  dvh0g  38407  dih0cnv  38579  dih1rn  38583  dih1cnv  38584  doch0  38654  doch1  38655  lcfl7lem  38795  mapdheq  39024  hdmap1eq  39097  hdmapval2lem  39127  hgmapvvlem3  39221  lcmineqlem13  39329  frlmsnic  39453  fsuppssind  39459  renegid  39511  sn-0ne2  39544  remul01  39545  remulinvcom  39569  sn-0tie0  39576  sn-inelr  39590  mzpval  39673  mzpindd  39687  pellex  39776  2nn0ind  39886  jm2.26lem3  39942  pw2f1o2val  39980  wepwsolem  39986  fnwe2lem3  39996  lnmfg  40026  dgrsub2  40079  mpaaeu  40094  flcidc  40118  rtrclexlem  40316  cnvrcl0  40325  brcoffn  40733  clsk1indlem3  40746  clsneif1o  40807  clsneicnv  40808  clsneikex  40809  clsneinex  40810  neicvgmex  40820  neicvgel1  40822  suprleubrd  40870  suprlubrd  40873  imo72b2  40878  dvconstbi  41038  bcc0  41044  binomcxplemnotnn0  41060  nnfoctb  41681  infleinflem1  42002  fprodcnlem  42241  sumnnodd  42272  icccncfext  42529  itgsin0pilem1  42592  stoweidlem32  42674  stoweidlem35  42677  stoweidlem36  42678  stoweidlem37  42679  stoweidlem43  42685  stoweidlem50  42692  wallispilem5  42711  stirlinglem2  42717  stirlinglem3  42718  stirlinglem4  42719  stirlinglem8  42723  stirlinglem11  42726  stirlinglem12  42727  stirlinglem14  42729  stirlinglem15  42730  fourierdlem11  42760  fourierdlem20  42769  fourierdlem21  42770  fourierdlem41  42790  fourierdlem42  42791  fourierdlem48  42796  fourierdlem49  42797  fourierdlem64  42812  fourierdlem71  42819  fourierdlem79  42827  fourierdlem90  42838  fourierdlem91  42839  fourierswlem  42872  etransclem17  42893  etransclem38  42914  saluni  42966  meaiininclem  43125  issmflelem  43378  issmfgtlem  43389  issmfgelem  43402  smflimsuplem4  43454  sprval  43996  prprval  44031  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbnd  44327  isomushgr  44344  isomuspgrlem1  44345  isclintop  44467  clintopcllaw  44471  nzrneg1ne0  44493  c0snmgmhm  44538  zrrnghm  44541  lidldomn1  44545  zlidlring  44552  uzlidlring  44553  2zrngnmlid  44573  cznrng  44579  zrinitorngc  44624  zrtermorngc  44625  zrtermoringc  44694  coe1id  44792  blenre  44988  blennn  44989  2arymaptf  45066  itcoval1  45077  itcovalendof  45083  ehl2eudisval0  45139  eenglngeehlnmlem2  45152  itsclc0yqsol  45178  inlinecirc02plem  45200