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  39198  renegid  39252  sn-0ne2  39285  remul01  39286  remulinvcom  39297  mzpval  39378  mzpindd  39392  pellex  39481  2nn0ind  39591  jm2.26lem3  39647  pw2f1o2val  39685  wepwsolem  39691  fnwe2lem3  39701  lnmfg  39731  dgrsub2  39784  mpaaeu  39799  flcidc  39823  rtrclexlem  40025  cnvrcl0  40034  brcoffn  40429  clsk1indlem3  40442  clsneif1o  40503  clsneicnv  40504  clsneikex  40505  clsneinex  40506  neicvgmex  40516  neicvgel1  40518  suprleubrd  40566  suprlubrd  40569  imo72b2  40574  dvconstbi  40715  bcc0  40721  binomcxplemnotnn0  40737  nnfoctb  41358  infleinflem1  41687  fprodcnlem  41929  sumnnodd  41960  icccncfext  42219  itgsin0pilem1  42284  stoweidlem32  42366  stoweidlem35  42369  stoweidlem36  42370  stoweidlem37  42371  stoweidlem43  42377  stoweidlem50  42384  wallispilem5  42403  stirlinglem2  42409  stirlinglem3  42410  stirlinglem4  42411  stirlinglem8  42415  stirlinglem11  42418  stirlinglem12  42419  stirlinglem14  42421  stirlinglem15  42422  fourierdlem11  42452  fourierdlem20  42461  fourierdlem21  42462  fourierdlem41  42482  fourierdlem42  42483  fourierdlem48  42488  fourierdlem49  42489  fourierdlem64  42504  fourierdlem71  42511  fourierdlem79  42519  fourierdlem90  42530  fourierdlem91  42531  fourierswlem  42564  etransclem17  42585  etransclem38  42606  saluni  42658  meaiininclem  42817  issmflelem  43070  issmfgtlem  43081  issmfgelem  43094  smflimsuplem4  43146  sprval  43690  prprval  43725  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbnd  44023  isomushgr  44040  isomuspgrlem1  44041  isclintop  44163  clintopcllaw  44167  nzrneg1ne0  44189  c0snmgmhm  44234  zrrnghm  44237  lidldomn1  44241  zlidlring  44248  uzlidlring  44249  2zrngnmlid  44269  cznrng  44275  zrinitorngc  44320  zrtermorngc  44321  zrtermoringc  44390  coe1id  44487  blenre  44683  blennn  44684  ehl2eudisval0  44761  eenglngeehlnmlem2  44774  itsclc0yqsol  44800  inlinecirc02plem  44822