Theorem mpdan 685

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpidan  687  mpan2  689  mpjaodan  955  mpjao3dan  1427  mpd3an3  1458  eueq2  3701  csbiegf  3916  difsnb  4739  reusv3i  5305  fimadmfo  6599  fimadmfoALT  6601  fvtresfn  6770  fvmpt3  6772  ffvelrnd  6852  fnressn  6920  fsnex  7039  f1oiso2  7105  riota5f  7142  onsucuni  7543  seqomlem2  8087  oaordi  8172  nnaordi  8244  qsdisj  8374  dom2lem  8549  canth2g  8671  limenpsi  8692  php4  8704  onfin  8709  sucxpdom  8727  xpfi  8789  dmfi  8802  pwfilem  8818  pwfi  8819  fiin  8886  supiso  8939  ordiso2  8979  wdom2d  9044  infeq5  9100  cantnfp1lem3  9143  cantnflem1d  9151  rankwflemb  9222  onenon  9378  cardonle  9386  sdomsdomcardi  9400  acni  9471  cardaleph  9515  djuen  9595  djuinf  9614  infdju1  9615  pwsdompw  9626  infdif  9631  cfval  9669  fin34  9812  fin1a2lem1  9822  fin1a2  9837  ttukeylem6  9936  sdomsdomcard  9982  canth3  9983  fpwwe2  10065  canthwelem  10072  gchdju1  10078  pwfseqlem4  10084  gchdjuidm  10090  gchxpidm  10091  tskwe2  10195  rankcf  10199  tskuni  10205  gruxp  10229  dmrecnq  10390  lterpq  10392  archnq  10402  reclem3pr  10471  reclem4pr  10472  0idsr  10519  lep1  11481  ledivp1  11542  negfi  11589  supaddc  11608  supmul1  11610  suprzcl  12063  uz11  12268  zmin  12345  zbtwnre  12347  rpnnen1lem4  12380  rpnnen1lem5  12381  xnegid  12632  supxrre  12721  infxrre  12730  eluzfz2  12916  fzsuc  12955  fzsuc2  12966  fzp1disj  12967  fzneuz  12989  nn0p1elfzo  13081  fllep1  13172  fraclt1  13173  fracle1  13174  fracge0  13175  flhalf  13201  ceige  13214  ceim1l  13216  fldiv  13229  modval  13240  suppssfz  13363  seqeq1  13373  expubnd  13542  iexpcyc  13570  binom2sub1  13583  faclbnd4lem3  13656  pfxid  14046  pfxccatpfx2  14099  swrdccat3blem  14101  cshw0  14156  cshwn  14159  cshimadifsn  14191  cshimadifsn0  14192  pfx2  14309  trclexlem  14354  shftfval  14429  shftcan1  14442  reval  14465  cjmulrcl  14503  addcj  14507  absval  14597  absneg  14637  abscj  14639  sqabsadd  14642  sqabssub  14643  leabs  14659  sqreulem  14719  lo1res  14916  o1of2  14969  o1rlimmul  14975  flo1  15209  trirecip  15218  efcan  15449  efi4p  15490  resin4p  15491  recos4p  15492  sincossq  15529  ruclem10  15592  iddvds  15623  1dvds  15624  2ebits  15796  lcmftp  15980  coprmgcdb  15993  1idssfct  16024  exprmfct  16048  eulerthlem2  16119  odzphi  16133  pcprendvds  16177  pcmpt  16228  oddprmdvds  16239  vdwlem8  16324  0ram2  16357  prmgaplem7  16393  setsn0fun  16520  setsexstruct2  16522  pwsvscaval  16768  2initoinv  17270  initoeu1  17271  initoeu2lem1  17274  initoeu2  17276  2termoinv  17277  termoeu1  17278  homarel  17296  joinfval  17611  meetfval  17625  latjcom  17669  latmcom  17685  0subm  17982  sgrp2nmndlem5  18094  grprcan  18137  isgrpid2  18140  grpinvid  18160  mulgnn0z  18254  0subg  18304  qus0  18338  ghmker  18384  symgbasmap  18505  symginv  18530  pmtrfrn  18586  odmulg2  18682  slwpgp  18738  pj1eq  18826  efgtf  18848  frgpinv  18890  frgpup2  18902  cnaddablx  18988  cnaddabl  18989  zaddablx  18992  dprdfadd  19142  dpjidcl  19180  dpjlid  19183  pgpfac1lem3  19199  srgen1zr  19280  1unit  19408  unitgrpid  19419  1rinv  19429  irredn0  19453  irredneg  19460  isdrng2  19512  rnrhmsubrg  19567  abv0  19602  abv1z  19603  abvneg  19605  lmodfopne  19672  lsssn0  19719  lspsn0  19780  lsp0  19781  lmhmvsca  19817  lmhmrnlss  19822  lmhmkerlss  19823  lsppratlem5  19923  rsp1  19997  ringen1zr  20050  rlmassa  20100  snifpsrbag  20146  psrvscaval  20172  psrdi  20186  psrdir  20187  mplvscaval  20228  mhpmpl  20335  mhpdeg  20336  coe1sclmulfv  20451  ply1idvr1  20461  evl1var  20499  cnfldneg  20571  zringcyg  20638  chrid  20674  chrrhm  20678  ip0r  20781  ocvlss  20816  ocv1  20823  mamuvs1  21014  mamuvs2  21015  matecl  21034  matvscacell  21045  mat0scmat  21147  submaval0  21189  mdetrsca  21212  maduval  21247  minmar1val0  21256  pmatcollpw3fi1lem2  21395  chcoeffeqlem  21493  cayleyhamilton0  21497  cayleyhamiltonALT  21499  toponsspwpw  21530  cctop  21614  cldval  21631  ntrfval  21632  clsfval  21633  cmclsopn  21670  opncldf3  21694  neifval  21707  lpfval  21746  cnrmnrm  21969  dis2ndc  22068  islocfin  22125  tx1cn  22217  idqtop  22314  kqtopon  22335  kqid  22336  kqcld  22343  hmphen2  22407  filssufil  22520  ufileu  22527  alexsublem  22652  efmndtmd  22709  symgtgp  22714  ustuqtop4  22853  cstucnd  22893  metustexhalf  23166  nm0  23238  rlmnlm  23297  nmolb  23326  metdseq0  23462  pi1xfrval  23658  clmvneg1  23703  clmvsubval  23713  ipcau2  23837  tcphcphlem1  23838  tcphcphlem2  23839  cmetcaulem  23891  ovolicc2lem3  24120  ovolicc2lem4  24121  mbfmulc2lem  24248  i1fpos  24307  mbfi1fseqlem3  24318  itg2ge0  24336  dvres2  24510  dvaddbr  24535  dvmulbr  24536  dvcobr  24543  dvfsumlem4  24626  ftc1a  24634  ftc1lem6  24638  uc1pmon1p  24745  ig1pval2  24767  dgradd2  24858  dgrcolem2  24864  plydivlem4  24885  plydiveu  24887  elqaalem3  24910  qaa  24912  ulmdvlem1  24988  abelthlem6  25024  abelthlem7  25026  eflogeq  25185  jensenlem2  25565  harmonicbnd4  25588  sgmnncl  25724  dchrptlem2  25841  1lgs  25916  lgs1  25917  2sqcoprm  26011  addsqnreup  26019  dchrisumlem2  26066  dchrisum0lem2a  26093  selberg2lem  26126  pntrsumo1  26141  pntrsumbnd  26142  pntpbnd1  26162  pntlemr  26178  pntlemj  26179  padicabvf  26207  incistruhgr  26864  subgrprop3  27058  subgruhgredgd  27066  usgrexi  27223  cusgrexi  27225  cusgrsizeinds  27234  vtxdgfusgrf  27279  1hevtxdg1  27288  1egrvtxdg1  27291  ewlkprop  27385  wlklenvm1  27403  wlkl1loop  27419  wlkp1lem4  27458  2pthnloop  27512  upgrclwlkcompim  27562  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0lem6  27593  crctcshwlkn0lem7  27594  crctcshlem4  27598  wspthnonp  27637  wlkswwlksf1o  27657  wwlksnwwlksnon  27694  umgr2wlkon  27729  wwlks2onv  27732  elwwlks2ons3im  27733  elwspths2spth  27746  umgrclwwlkge2  27769  clwlkclwwlkf1lem3  27784  erclwwlkref  27798  clwwlknp  27815  wwlksext2clwwlk  27836  wwlksubclwwlk  27837  0pthon1  27907  1wlkdlem4  27919  1pthd  27922  3spthd  27955  eupth2eucrct  27996  eucrctshift  28022  eucrct2eupth  28024  frgrncvvdeqlem8  28085  frgr2wwlkeqm  28110  isgrpoi  28275  grpoinvfval  28299  grpodivfval  28311  vcz  28352  cnaddabloOLD  28358  nvz0  28445  sspz  28512  lno0  28533  nmobndi  28552  ipasslem2  28609  shunssi  29145  ococin  29185  ssjo  29224  pjocini  29475  nlfnval  29658  lncnopbd  29814  riesz3i  29839  cnlnadjlem7  29850  pjclem4  29976  pj3si  29984  hstoc  29999  hstnmoc  30000  hstoh  30009  hst0  30010  mdsl2i  30099  chirredlem3  30169  chirredlem4  30170  dmdbr5ati  30199  rexunirn  30256  fcnvgreu  30418  infxrge0glb  30489  omndmul2  30713  omndmul  30715  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  isarchi3  30816  orng0le1  30885  ssmxidllem  30978  fedgmullem1  31025  extdg1id  31053  esumcvg  31345  esumcvgre  31350  sigaval  31370  unelldsys  31417  fiunelros  31433  measval  31457  pmeasmono  31582  probfinmeasb  31686  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemsi  31772  ballotlemfrci  31785  sgnneg  31798  signlem0  31857  breprexp  31904  bnj1006  32232  bnj1110  32254  bnj1253  32289  bnj1280  32292  bnj1463  32327  bnj1312  32330  erdszelem7  32444  erdszelem8  32445  cvmliftlem10  32541  cvmliftlem13  32543  cvmlift2lem9  32558  cvmlift3lem6  32571  cvmlift3lem7  32572  cvmlift3lem9  32574  satfv1lem  32609  dfrdg2  33040  dftrpred3g  33072  frpoinsg  33081  frrlem10  33132  bdayval  33155  noextendgt  33177  nosupbnd2lem1  33215  cldregopn  33679  tailfval  33720  filnetlem3  33728  filnetlem4  33729  ontopbas  33776  bj-elid4  34463  f1omptsnlem  34620  icoreunrn  34643  relowlpssretop  34648  fvineqsnf1  34694  wl-sbal2  34815  unccur  34890  poimirlem1  34908  poimirlem2  34909  poimirlem4  34911  poimirlem6  34913  poimirlem7  34914  poimirlem11  34918  poimirlem12  34919  poimirlem17  34924  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimirlem28  34935  poimir  34940  ismblfin  34948  cnambfre  34955  bddiblnc  34977  ftc1cnnc  34981  dvasin  34993  ismtyres  35101  heiborlem8  35111  ghomidOLD  35182  rngosn6  35219  rngonegmn1l  35234  rngonegmn1r  35235  rngoneglmul  35236  rngonegrmul  35237  idlnegcl  35315  0idl  35318  0rngo  35320  smprngopr  35345  cossex  35679  qsdisjALTV  35865  cnvepresdmqss  35901  lkrval  36239  ldualvaddval  36282  ldualvsval  36289  opoc1  36353  pmap0  36916  pmap1N  36918  pexmidALTN  37129  cdleme31fv  37541  cdlemg27b  37847  erngdvlem4  38142  erng0g  38145  erngdvlem4-rN  38150  dvalveclem  38176  dvh0g  38262  dih0cnv  38434  dih1rn  38438  dih1cnv  38439  doch0  38509  doch1  38510  lcfl7lem  38650  mapdheq  38879  hdmap1eq  38952  hdmapval2lem  38982  hgmapvvlem3  39076  frlmsnic  39169  renegid  39223  sn-0ne2  39256  remul01  39257  remulinvcom  39268  mzpval  39349  mzpindd  39363  pellex  39452  2nn0ind  39562  jm2.26lem3  39618  pw2f1o2val  39656  wepwsolem  39662  fnwe2lem3  39672  lnmfg  39702  dgrsub2  39755  mpaaeu  39770  flcidc  39794  rtrclexlem  39996  cnvrcl0  40005  brcoffn  40400  clsk1indlem3  40413  clsneif1o  40474  clsneicnv  40475  clsneikex  40476  clsneinex  40477  neicvgmex  40487  neicvgel1  40489  suprleubrd  40537  suprlubrd  40540  imo72b2  40545  dvconstbi  40686  bcc0  40692  binomcxplemnotnn0  40708  nnfoctb  41329  infleinflem1  41658  fprodcnlem  41900  sumnnodd  41931  icccncfext  42190  itgsin0pilem1  42255  stoweidlem32  42337  stoweidlem35  42340  stoweidlem36  42341  stoweidlem37  42342  stoweidlem43  42348  stoweidlem50  42355  wallispilem5  42374  stirlinglem2  42380  stirlinglem3  42381  stirlinglem4  42382  stirlinglem8  42386  stirlinglem11  42389  stirlinglem12  42390  stirlinglem14  42392  stirlinglem15  42393  fourierdlem11  42423  fourierdlem20  42432  fourierdlem21  42433  fourierdlem41  42453  fourierdlem42  42454  fourierdlem48  42459  fourierdlem49  42460  fourierdlem64  42475  fourierdlem71  42482  fourierdlem79  42490  fourierdlem90  42501  fourierdlem91  42502  fourierswlem  42535  etransclem17  42556  etransclem38  42577  saluni  42629  meaiininclem  42788  issmflelem  43041  issmfgtlem  43052  issmfgelem  43065  smflimsuplem4  43117  sprval  43661  prprval  43696  bgoldbtbndlem2  43991  bgoldbtbndlem3  43992  bgoldbtbnd  43994  isomushgr  44011  isomuspgrlem1  44012  isclintop  44134  clintopcllaw  44138  nzrneg1ne0  44160  c0snmgmhm  44205  zrrnghm  44208  lidldomn1  44212  zlidlring  44219  uzlidlring  44220  2zrngnmlid  44240  cznrng  44246  zrinitorngc  44291  zrtermorngc  44292  zrtermoringc  44361  coe1id  44458  blenre  44654  blennn  44655  ehl2eudisval0  44732  eenglngeehlnmlem2  44745  itsclc0yqsol  44771  inlinecirc02plem  44793