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 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  689  mpan2  691  biadanid  823  mpjaodan  959  mpjao3dan  1433  mpd3an3  1464  elabd2  3579  eueq2  3623  csbiegf  3845  difsnb  4719  reusv3i  5297  frpoinsg  6197  fimadmfo  6642  fimadmfoALT  6644  fvtresfn  6820  fvmpt3  6822  ffvelrnd  6905  fnressn  6973  fsnex  7093  f1oiso2  7161  riota5f  7199  onsucuni  7607  frrlem10  8036  seqomlem2  8187  oaordi  8274  nnaordi  8346  qsdisj  8476  dom2lem  8668  canth2g  8800  limenpsi  8821  php4  8833  nnfi  8845  onfin  8870  sucxpdom  8887  xpfi  8942  dmfi  8954  pwfilemOLD  8970  pwfiOLD  8971  fiin  9038  supiso  9091  ordiso2  9131  wdom2d  9196  infeq5  9252  cantnfp1lem3  9295  cantnflem1d  9303  dftrpred3g  9339  rankwflemb  9409  onenon  9565  cardonle  9573  sdomsdomcardi  9587  acni  9659  cardaleph  9703  djuen  9783  djuinf  9802  infdju1  9803  nnadju  9811  pwsdompw  9818  infdif  9823  cfval  9861  fin34  10004  fin1a2lem1  10014  fin1a2  10029  ttukeylem6  10128  sdomsdomcard  10174  canth3  10175  fpwwe2  10257  canthwelem  10264  gchdju1  10270  pwfseqlem4  10276  gchdjuidm  10282  gchxpidm  10283  tskwe2  10387  rankcf  10391  tskuni  10397  gruxp  10421  dmrecnq  10582  lterpq  10584  archnq  10594  reclem3pr  10663  reclem4pr  10664  0idsr  10711  lep1  11673  ledivp1  11734  negfi  11781  supaddc  11799  supmul1  11801  suprzcl  12257  uz11  12463  zmin  12540  zbtwnre  12542  rpnnen1lem4  12576  rpnnen1lem5  12577  xnegid  12828  supxrre  12917  infxrre  12926  eluzfz2  13120  fzsuc  13159  fzsuc2  13170  fzp1disj  13171  fzneuz  13193  nn0p1elfzo  13285  fllep1  13376  fraclt1  13377  fracle1  13378  fracge0  13379  flhalf  13405  ceige  13418  ceim1l  13420  fldiv  13433  modval  13444  suppssfz  13567  seqeq1  13577  expubnd  13747  iexpcyc  13775  binom2sub1  13788  faclbnd4lem3  13861  pfxid  14249  pfxccatpfx2  14302  swrdccat3blem  14304  cshw0  14359  cshwn  14362  cshimadifsn  14394  cshimadifsn0  14395  pfx2  14512  trclexlem  14557  shftfval  14633  shftcan1  14646  reval  14669  cjmulrcl  14707  addcj  14711  absval  14801  absneg  14841  abscj  14843  sqabsadd  14846  sqabssub  14847  leabs  14863  sqreulem  14923  lo1res  15120  o1of2  15174  o1rlimmul  15180  flo1  15418  trirecip  15427  efcan  15657  efi4p  15698  resin4p  15699  recos4p  15700  sincossq  15737  ruclem10  15800  iddvds  15831  1dvds  15832  2ebits  16006  lcmftp  16193  coprmgcdb  16206  1idssfct  16237  exprmfct  16261  eulerthlem2  16335  odzphi  16349  pcprendvds  16393  pcmpt  16445  oddprmdvds  16456  vdwlem8  16541  0ram2  16574  prmgaplem7  16610  setsn0fun  16726  setsexstruct2  16728  pwsvscaval  17000  2initoinv  17516  initoeu1  17517  initoeu2lem1  17520  initoeu2  17522  2termoinv  17523  termoeu1  17524  homarel  17542  joinfval  17879  meetfval  17893  latjcom  17953  latmcom  17969  0subm  18244  sgrp2nmndlem5  18356  grprcan  18401  isgrpid2  18404  grpinvid  18424  mulgnn0z  18518  0subg  18568  qus0  18602  ghmker  18648  symgbasmap  18769  symginv  18794  pmtrfrn  18850  odmulg2  18946  slwpgp  19002  pj1eq  19090  efgtf  19112  frgpinv  19154  frgpup2  19166  cnaddablx  19253  cnaddabl  19254  zaddablx  19257  dprdfadd  19407  dpjidcl  19445  dpjlid  19448  pgpfac1lem3  19464  srgen1zr  19545  1unit  19676  unitgrpid  19687  1rinv  19697  irredn0  19721  irredneg  19728  isdrng2  19777  rnrhmsubrg  19832  abv0  19867  abv1z  19868  abvneg  19870  lmodfopne  19937  lsssn0  19984  lspsn0  20045  lsp0  20046  lmhmvsca  20082  lmhmrnlss  20087  lmhmkerlss  20088  lsppratlem5  20188  rsp1  20262  ringen1zr  20315  cnfldneg  20389  zringcyg  20456  chrid  20492  chrrhm  20496  ip0r  20599  ocvlss  20634  ocv1  20641  rlmassa  20830  psrbagfsupp  20879  snifpsrbag  20881  psrbaglefi  20891  psrvscaval  20917  psrdi  20931  psrdir  20932  mplvscaval  20976  mhpmpl  21084  mhpdeg  21085  mhppwdeg  21090  coe1sclmulfv  21204  ply1idvr1  21214  evl1var  21252  mamuvs1  21302  mamuvs2  21303  matecl  21322  matvscacell  21333  mat0scmat  21435  submaval0  21477  mdetrsca  21500  maduval  21535  minmar1val0  21544  pmatcollpw3fi1lem2  21684  chcoeffeqlem  21782  cayleyhamilton0  21786  cayleyhamiltonALT  21788  toponsspwpw  21819  cctop  21903  cldval  21920  ntrfval  21921  clsfval  21922  cmclsopn  21959  opncldf3  21983  neifval  21996  lpfval  22035  cnrmnrm  22258  dis2ndc  22357  islocfin  22414  tx1cn  22506  idqtop  22603  kqtopon  22624  kqid  22625  kqcld  22632  hmphen2  22696  filssufil  22809  ufileu  22816  alexsublem  22941  efmndtmd  22998  symgtgp  23003  ustuqtop4  23142  cstucnd  23181  metustexhalf  23454  nm0  23527  rlmnlm  23586  nmolb  23615  metdseq0  23751  pi1xfrval  23951  clmvneg1  23996  clmvsubval  24006  ipcau2  24131  tcphcphlem1  24132  tcphcphlem2  24133  cmetcaulem  24185  ovolicc2lem3  24416  ovolicc2lem4  24417  mbfmulc2lem  24544  i1fpos  24604  mbfi1fseqlem3  24615  itg2ge0  24633  bddiblnc  24739  dvres2  24809  dvaddbr  24835  dvmulbr  24836  dvcobr  24843  dvfsumlem4  24926  ftc1a  24934  ftc1lem6  24938  uc1pmon1p  25049  ig1pval2  25071  dgradd2  25162  dgrcolem2  25168  plydivlem4  25189  plydiveu  25191  elqaalem3  25214  qaa  25216  ulmdvlem1  25292  abelthlem6  25328  abelthlem7  25330  eflogeq  25490  jensenlem2  25870  harmonicbnd4  25893  sgmnncl  26029  dchrptlem2  26146  1lgs  26221  lgs1  26222  2sqcoprm  26316  addsqnreup  26324  dchrisumlem2  26371  dchrisum0lem2a  26398  selberg2lem  26431  pntrsumo1  26446  pntrsumbnd  26447  pntpbnd1  26467  pntlemr  26483  pntlemj  26484  padicabvf  26512  incistruhgr  27170  subgrprop3  27364  subgruhgredgd  27372  usgrexi  27529  cusgrexi  27531  cusgrsizeinds  27540  vtxdgfusgrf  27585  1hevtxdg1  27594  1egrvtxdg1  27597  ewlkprop  27691  wlklenvm1  27709  wlkl1loop  27725  wlkp1lem4  27764  2pthnloop  27818  upgrclwlkcompim  27868  crctcshwlkn0lem4  27897  crctcshwlkn0lem5  27898  crctcshwlkn0lem6  27899  crctcshwlkn0lem7  27900  crctcshlem4  27904  wspthnonp  27943  wlkswwlksf1o  27963  wwlksnwwlksnon  27999  umgr2wlkon  28034  wwlks2onv  28037  elwwlks2ons3im  28038  elwspths2spth  28051  umgrclwwlkge2  28074  clwlkclwwlkf1lem3  28089  erclwwlkref  28103  clwwlknp  28120  wwlksext2clwwlk  28140  wwlksubclwwlk  28141  0pthon1  28211  1wlkdlem4  28223  1pthd  28226  3spthd  28259  eupth2eucrct  28300  eucrctshift  28326  eucrct2eupth  28328  frgrncvvdeqlem8  28389  frgr2wwlkeqm  28414  isgrpoi  28579  grpoinvfval  28603  grpodivfval  28615  vcz  28656  cnaddabloOLD  28662  nvz0  28749  sspz  28816  lno0  28837  nmobndi  28856  ipasslem2  28913  shunssi  29449  ococin  29489  ssjo  29528  pjocini  29779  nlfnval  29962  lncnopbd  30118  riesz3i  30143  cnlnadjlem7  30154  pjclem4  30280  pj3si  30288  hstoc  30303  hstnmoc  30304  hstoh  30313  hst0  30314  mdsl2i  30403  chirredlem3  30473  chirredlem4  30474  dmdbr5ati  30503  rexunirn  30559  fcnvgreu  30730  infxrge0glb  30808  omndmul2  31057  omndmul  31059  cycpmco2lem5  31116  cycpmco2lem6  31117  cycpmco2lem7  31118  isarchi3  31160  orng0le1  31230  nsgqusf1olem2  31313  kerlidl  31318  ssmxidllem  31355  fedgmullem1  31424  extdg1id  31452  zartopn  31539  zarcmplem  31545  esumcvg  31766  esumcvgre  31771  sigaval  31791  unelldsys  31838  fiunelros  31854  measval  31878  pmeasmono  32003  probfinmeasb  32107  ballotlemfc0  32171  ballotlemfcc  32172  ballotlemsi  32193  ballotlemfrci  32206  sgnneg  32219  signlem0  32278  breprexp  32325  bnj1006  32653  bnj1110  32675  bnj1253  32710  bnj1280  32713  bnj1463  32748  bnj1312  32751  erdszelem7  32872  erdszelem8  32873  cvmliftlem10  32969  cvmliftlem13  32971  cvmlift2lem9  32986  cvmlift3lem6  32999  cvmlift3lem7  33000  cvmlift3lem9  33002  satfv1lem  33037  dfrdg2  33490  bdayval  33588  noextendgt  33610  nosupbnd2lem1  33655  noinfbnd2lem1  33670  noetainflem4  33680  oldval  33775  cldregopn  34257  tailfval  34298  filnetlem3  34306  filnetlem4  34307  ontopbas  34354  bj-elid4  35074  bj-imdiridlem  35091  f1omptsnlem  35244  icoreunrn  35267  relowlpssretop  35272  fvineqsnf1  35318  wl-sbal2  35456  unccur  35497  poimirlem1  35515  poimirlem2  35516  poimirlem4  35518  poimirlem6  35520  poimirlem7  35521  poimirlem11  35525  poimirlem12  35526  poimirlem17  35531  poimirlem20  35534  poimirlem22  35536  poimirlem23  35537  poimirlem28  35542  poimir  35547  ismblfin  35555  cnambfre  35562  ftc1cnnc  35586  dvasin  35598  ismtyres  35703  heiborlem8  35713  ghomidOLD  35784  rngosn6  35821  rngonegmn1l  35836  rngonegmn1r  35837  rngoneglmul  35838  rngonegrmul  35839  idlnegcl  35917  0idl  35920  0rngo  35922  smprngopr  35947  cossex  36279  qsdisjALTV  36465  cnvepresdmqss  36501  lkrval  36839  ldualvaddval  36882  ldualvsval  36889  opoc1  36953  pmap0  37516  pmap1N  37518  pexmidALTN  37729  cdleme31fv  38141  cdlemg27b  38447  erngdvlem4  38742  erng0g  38745  erngdvlem4-rN  38750  dvalveclem  38776  dvh0g  38862  dih0cnv  39034  dih1rn  39038  dih1cnv  39039  doch0  39109  doch1  39110  lcfl7lem  39250  mapdheq  39479  hdmap1eq  39552  hdmapval2lem  39582  hgmapvvlem3  39676  lcmineqlem13  39783  sticksstones1  39824  sticksstones6  39829  sticksstones7  39830  sticksstones11  39834  sticksstones12a  39835  sticksstones12  39836  sticksstones22  39846  frlmsnic  39975  fsuppssind  39992  renegid  40064  sn-0ne2  40097  remul01  40098  remulinvcom  40122  sn-0tie0  40129  sn-inelr  40143  mzpval  40257  mzpindd  40271  pellex  40360  2nn0ind  40470  jm2.26lem3  40526  pw2f1o2val  40564  wepwsolem  40570  fnwe2lem3  40580  lnmfg  40610  dgrsub2  40663  mpaaeu  40678  flcidc  40702  rtrclexlem  40900  cnvrcl0  40909  brcoffn  41317  clsk1indlem3  41330  clsneif1o  41391  clsneicnv  41392  clsneikex  41393  clsneinex  41394  neicvgmex  41404  neicvgel1  41406  suprleubrd  41454  suprlubrd  41456  imo72b2  41461  dvconstbi  41625  bcc0  41631  binomcxplemnotnn0  41647  nnfoctb  42268  infleinflem1  42582  fprodcnlem  42815  sumnnodd  42846  icccncfext  43103  itgsin0pilem1  43166  stoweidlem32  43248  stoweidlem35  43251  stoweidlem36  43252  stoweidlem37  43253  stoweidlem43  43259  stoweidlem50  43266  wallispilem5  43285  stirlinglem2  43291  stirlinglem3  43292  stirlinglem4  43293  stirlinglem8  43297  stirlinglem11  43300  stirlinglem12  43301  stirlinglem14  43303  stirlinglem15  43304  fourierdlem11  43334  fourierdlem20  43343  fourierdlem21  43344  fourierdlem41  43364  fourierdlem42  43365  fourierdlem48  43370  fourierdlem49  43371  fourierdlem64  43386  fourierdlem71  43393  fourierdlem79  43401  fourierdlem90  43412  fourierdlem91  43413  fourierswlem  43446  etransclem17  43467  etransclem38  43488  saluni  43540  meaiininclem  43699  issmflelem  43952  issmfgtlem  43963  issmfgelem  43976  smflimsuplem4  44028  f1cof1blem  44240  sprval  44604  prprval  44639  bgoldbtbndlem2  44931  bgoldbtbndlem3  44932  bgoldbtbnd  44934  isomushgr  44951  isomuspgrlem1  44952  isclintop  45074  clintopcllaw  45078  nzrneg1ne0  45100  c0snmgmhm  45145  zrrnghm  45148  lidldomn1  45152  zlidlring  45159  uzlidlring  45160  2zrngnmlid  45180  cznrng  45186  zrinitorngc  45231  zrtermorngc  45232  zrtermoringc  45301  coe1id  45398  blenre  45593  blennn  45594  2arymaptf  45671  itcoval1  45682  itcovalendof  45688  ehl2eudisval0  45744  eenglngeehlnmlem2  45757  itsclc0yqsol  45783  inlinecirc02plem  45805  ipolub  45947  ipoglb  45950