Theorem mpdan 683

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

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  mpidan  685  mpan2  687  biadanid  819  mpjaodan  955  mpjao3dan  1429  mpd3an3  1460  elabd2  3594  eueq2  3640  csbiegf  3862  difsnb  4736  reusv3i  5322  frpoinsg  6231  fimadmfo  6681  fimadmfoALT  6683  fvtresfn  6859  fvmpt3  6861  ffvelrnd  6944  fnressn  7012  fsnex  7135  f1oiso2  7203  riota5f  7241  onsucuni  7650  frrlem10  8082  seqomlem2  8252  oaordi  8339  nnaordi  8411  qsdisj  8541  dom2lem  8735  canth2g  8867  limenpsi  8888  php4  8900  nnfi  8912  onfin  8944  sucxpdom  8961  xpfi  9015  dmfi  9027  pwfilemOLD  9043  pwfiOLD  9044  fiin  9111  supiso  9164  ordiso2  9204  wdom2d  9269  infeq5  9325  cantnfp1lem3  9368  cantnflem1d  9376  dftrpred3g  9412  rankwflemb  9482  onenon  9638  cardonle  9646  sdomsdomcardi  9660  acni  9732  cardaleph  9776  djuen  9856  djuinf  9875  infdju1  9876  nnadju  9884  pwsdompw  9891  infdif  9896  cfval  9934  fin34  10077  fin1a2lem1  10087  fin1a2  10102  ttukeylem6  10201  sdomsdomcard  10247  canth3  10248  fpwwe2  10330  canthwelem  10337  gchdju1  10343  pwfseqlem4  10349  gchdjuidm  10355  gchxpidm  10356  tskwe2  10460  rankcf  10464  tskuni  10470  gruxp  10494  dmrecnq  10655  lterpq  10657  archnq  10667  reclem3pr  10736  reclem4pr  10737  0idsr  10784  lep1  11746  ledivp1  11807  negfi  11854  supaddc  11872  supmul1  11874  suprzcl  12330  uz11  12536  zmin  12613  zbtwnre  12615  rpnnen1lem4  12649  rpnnen1lem5  12650  xnegid  12901  supxrre  12990  infxrre  12999  eluzfz2  13193  fzsuc  13232  fzsuc2  13243  fzp1disj  13244  fzneuz  13266  nn0p1elfzo  13358  fllep1  13449  fraclt1  13450  fracle1  13451  fracge0  13452  flhalf  13478  ceige  13492  ceim1l  13495  fldiv  13508  modval  13519  suppssfz  13642  seqeq1  13652  expubnd  13823  iexpcyc  13851  binom2sub1  13864  faclbnd4lem3  13937  pfxid  14325  pfxccatpfx2  14378  swrdccat3blem  14380  cshw0  14435  cshwn  14438  cshimadifsn  14470  cshimadifsn0  14471  pfx2  14588  trclexlem  14633  shftfval  14709  shftcan1  14722  reval  14745  cjmulrcl  14783  addcj  14787  absval  14877  absneg  14917  abscj  14919  sqabsadd  14922  sqabssub  14923  leabs  14939  sqreulem  14999  lo1res  15196  o1of2  15250  o1rlimmul  15256  flo1  15494  trirecip  15503  efcan  15733  efi4p  15774  resin4p  15775  recos4p  15776  sincossq  15813  ruclem10  15876  iddvds  15907  1dvds  15908  2ebits  16082  lcmftp  16269  coprmgcdb  16282  1idssfct  16313  exprmfct  16337  eulerthlem2  16411  odzphi  16425  pcprendvds  16469  pcmpt  16521  oddprmdvds  16532  vdwlem8  16617  0ram2  16650  prmgaplem7  16686  setsn0fun  16802  setsexstruct2  16804  pwsvscaval  17123  2initoinv  17641  initoeu1  17642  initoeu2lem1  17645  initoeu2  17647  2termoinv  17648  termoeu1  17649  homarel  17667  joinfval  18006  meetfval  18020  latjcom  18080  latmcom  18096  0subm  18371  sgrp2nmndlem5  18483  grprcan  18528  isgrpid2  18531  grpinvid  18551  mulgnn0z  18645  0subg  18695  qus0  18729  ghmker  18775  symgbasmap  18899  symginv  18925  pmtrfrn  18981  odmulg2  19077  slwpgp  19133  pj1eq  19221  efgtf  19243  frgpinv  19285  frgpup2  19297  cnaddablx  19384  cnaddabl  19385  zaddablx  19388  dprdfadd  19538  dpjidcl  19576  dpjlid  19579  pgpfac1lem3  19595  srgen1zr  19681  1unit  19815  unitgrpid  19826  1rinv  19836  irredn0  19860  irredneg  19867  isdrng2  19916  rnrhmsubrg  19971  abv0  20006  abv1z  20007  abvneg  20009  lmodfopne  20076  lsssn0  20124  lspsn0  20185  lsp0  20186  lmhmvsca  20222  lmhmrnlss  20227  lmhmkerlss  20228  lsppratlem5  20328  rsp1  20408  ringen1zr  20461  cnfldneg  20536  zringcyg  20603  chrid  20643  chrrhm  20647  ip0r  20754  ocvlss  20789  ocv1  20796  rlmassa  20985  psrbagfsupp  21033  snifpsrbag  21035  psrbaglefi  21045  psrvscaval  21071  psrdi  21085  psrdir  21086  mplvscaval  21130  mhpmpl  21244  mhpdeg  21245  mhppwdeg  21250  coe1sclmulfv  21364  ply1idvr1  21374  evl1var  21412  mamuvs1  21462  mamuvs2  21463  matecl  21482  matvscacell  21493  mat0scmat  21595  submaval0  21637  mdetrsca  21660  maduval  21695  minmar1val0  21704  pmatcollpw3fi1lem2  21844  chcoeffeqlem  21942  cayleyhamilton0  21946  cayleyhamiltonALT  21948  toponsspwpw  21979  cctop  22064  cldval  22082  ntrfval  22083  clsfval  22084  cmclsopn  22121  opncldf3  22145  neifval  22158  lpfval  22197  cnrmnrm  22420  dis2ndc  22519  islocfin  22576  tx1cn  22668  idqtop  22765  kqtopon  22786  kqid  22787  kqcld  22794  hmphen2  22858  filssufil  22971  ufileu  22978  alexsublem  23103  efmndtmd  23160  symgtgp  23165  ustuqtop4  23304  cstucnd  23344  metustexhalf  23618  nm0  23691  rlmnlm  23758  nmolb  23787  metdseq0  23923  pi1xfrval  24123  clmvneg1  24168  clmvsubval  24178  ipcau2  24303  tcphcphlem1  24304  tcphcphlem2  24305  cmetcaulem  24357  ovolicc2lem3  24588  ovolicc2lem4  24589  mbfmulc2lem  24716  i1fpos  24776  mbfi1fseqlem3  24787  itg2ge0  24805  bddiblnc  24911  dvres2  24981  dvaddbr  25007  dvmulbr  25008  dvcobr  25015  dvfsumlem4  25098  ftc1a  25106  ftc1lem6  25110  uc1pmon1p  25221  ig1pval2  25243  dgradd2  25334  dgrcolem2  25340  plydivlem4  25361  plydiveu  25363  elqaalem3  25386  qaa  25388  ulmdvlem1  25464  abelthlem6  25500  abelthlem7  25502  eflogeq  25662  jensenlem2  26042  harmonicbnd4  26065  sgmnncl  26201  dchrptlem2  26318  1lgs  26393  lgs1  26394  2sqcoprm  26488  addsqnreup  26496  dchrisumlem2  26543  dchrisum0lem2a  26570  selberg2lem  26603  pntrsumo1  26618  pntrsumbnd  26619  pntpbnd1  26639  pntlemr  26655  pntlemj  26656  padicabvf  26684  incistruhgr  27352  subgrprop3  27546  subgruhgredgd  27554  usgrexi  27711  cusgrexi  27713  cusgrsizeinds  27722  vtxdgfusgrf  27767  1hevtxdg1  27776  1egrvtxdg1  27779  ewlkprop  27873  wlklenvm1  27891  wlkl1loop  27907  wlkp1lem4  27946  2pthnloop  28000  upgrclwlkcompim  28050  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0lem6  28081  crctcshwlkn0lem7  28082  crctcshlem4  28086  wspthnonp  28125  wlkswwlksf1o  28145  wwlksnwwlksnon  28181  umgr2wlkon  28216  wwlks2onv  28219  elwwlks2ons3im  28220  elwspths2spth  28233  umgrclwwlkge2  28256  clwlkclwwlkf1lem3  28271  erclwwlkref  28285  clwwlknp  28302  wwlksext2clwwlk  28322  wwlksubclwwlk  28323  0pthon1  28393  1wlkdlem4  28405  1pthd  28408  3spthd  28441  eupth2eucrct  28482  eucrctshift  28508  eucrct2eupth  28510  frgrncvvdeqlem8  28571  frgr2wwlkeqm  28596  isgrpoi  28761  grpoinvfval  28785  grpodivfval  28797  vcz  28838  cnaddabloOLD  28844  nvz0  28931  sspz  28998  lno0  29019  nmobndi  29038  ipasslem2  29095  shunssi  29631  ococin  29671  ssjo  29710  pjocini  29961  nlfnval  30144  lncnopbd  30300  riesz3i  30325  cnlnadjlem7  30336  pjclem4  30462  pj3si  30470  hstoc  30485  hstnmoc  30486  hstoh  30495  hst0  30496  mdsl2i  30585  chirredlem3  30655  chirredlem4  30656  dmdbr5ati  30685  rexunirn  30741  fcnvgreu  30912  infxrge0glb  30990  omndmul2  31240  omndmul  31242  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  isarchi3  31343  orng0le1  31413  nsgqusf1olem2  31501  kerlidl  31506  ssmxidllem  31543  fedgmullem1  31612  extdg1id  31640  zartopn  31727  zarcmplem  31733  esumcvg  31954  esumcvgre  31959  sigaval  31979  unelldsys  32026  fiunelros  32042  measval  32066  pmeasmono  32191  probfinmeasb  32295  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemsi  32381  ballotlemfrci  32394  sgnneg  32407  signlem0  32466  breprexp  32513  bnj1006  32840  bnj1110  32862  bnj1253  32897  bnj1280  32900  bnj1463  32935  bnj1312  32938  erdszelem7  33059  erdszelem8  33060  cvmliftlem10  33156  cvmliftlem13  33158  cvmlift2lem9  33173  cvmlift3lem6  33186  cvmlift3lem7  33187  cvmlift3lem9  33189  satfv1lem  33224  dfrdg2  33677  bdayval  33778  noextendgt  33800  nosupbnd2lem1  33845  noinfbnd2lem1  33860  noetainflem4  33870  oldval  33965  cldregopn  34447  tailfval  34488  filnetlem3  34496  filnetlem4  34497  ontopbas  34544  bj-elid4  35266  bj-imdiridlem  35283  f1omptsnlem  35434  icoreunrn  35457  relowlpssretop  35462  fvineqsnf1  35508  wl-sbal2  35646  unccur  35687  poimirlem1  35705  poimirlem2  35706  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem11  35715  poimirlem12  35716  poimirlem17  35721  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem28  35732  poimir  35737  ismblfin  35745  cnambfre  35752  ftc1cnnc  35776  dvasin  35788  ismtyres  35893  heiborlem8  35903  ghomidOLD  35974  rngosn6  36011  rngonegmn1l  36026  rngonegmn1r  36027  rngoneglmul  36028  rngonegrmul  36029  idlnegcl  36107  0idl  36110  0rngo  36112  smprngopr  36137  cossex  36469  qsdisjALTV  36655  cnvepresdmqss  36691  lkrval  37029  ldualvaddval  37072  ldualvsval  37079  opoc1  37143  pmap0  37706  pmap1N  37708  pexmidALTN  37919  cdleme31fv  38331  cdlemg27b  38637  erngdvlem4  38932  erng0g  38935  erngdvlem4-rN  38940  dvalveclem  38966  dvh0g  39052  dih0cnv  39224  dih1rn  39228  dih1cnv  39229  doch0  39299  doch1  39300  lcfl7lem  39440  mapdheq  39669  hdmap1eq  39742  hdmapval2lem  39772  hgmapvvlem3  39866  lcmineqlem13  39977  aks4d1p9  40024  sticksstones1  40030  sticksstones6  40035  sticksstones7  40036  sticksstones11  40040  sticksstones12a  40041  sticksstones12  40042  sticksstones22  40052  frlmsnic  40188  fsuppssind  40205  renegid  40277  sn-0ne2  40310  remul01  40311  remulinvcom  40335  sn-0tie0  40342  sn-inelr  40356  mzpval  40470  mzpindd  40484  pellex  40573  2nn0ind  40683  jm2.26lem3  40739  pw2f1o2val  40777  wepwsolem  40783  fnwe2lem3  40793  lnmfg  40823  dgrsub2  40876  mpaaeu  40891  flcidc  40915  rtrclexlem  41113  cnvrcl0  41122  brcoffn  41529  clsk1indlem3  41542  clsneif1o  41603  clsneicnv  41604  clsneikex  41605  clsneinex  41606  neicvgmex  41616  neicvgel1  41618  suprleubrd  41666  suprlubrd  41668  imo72b2  41672  dvconstbi  41841  bcc0  41847  binomcxplemnotnn0  41863  nnfoctb  42484  infleinflem1  42799  fprodcnlem  43030  sumnnodd  43061  icccncfext  43318  itgsin0pilem1  43381  stoweidlem32  43463  stoweidlem35  43466  stoweidlem36  43467  stoweidlem37  43468  stoweidlem43  43474  stoweidlem50  43481  wallispilem5  43500  stirlinglem2  43506  stirlinglem3  43507  stirlinglem4  43508  stirlinglem8  43512  stirlinglem11  43515  stirlinglem12  43516  stirlinglem14  43518  stirlinglem15  43519  fourierdlem11  43549  fourierdlem20  43558  fourierdlem21  43559  fourierdlem41  43579  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem64  43601  fourierdlem71  43608  fourierdlem79  43616  fourierdlem90  43627  fourierdlem91  43628  fourierswlem  43661  etransclem17  43682  etransclem38  43703  saluni  43755  meaiininclem  43914  issmflelem  44167  issmfgtlem  44178  issmfgelem  44191  smflimsuplem4  44243  f1cof1blem  44455  sprval  44819  prprval  44854  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbnd  45149  isomushgr  45166  isomuspgrlem1  45167  isclintop  45289  clintopcllaw  45293  nzrneg1ne0  45315  c0snmgmhm  45360  zrrnghm  45363  lidldomn1  45367  zlidlring  45374  uzlidlring  45375  2zrngnmlid  45395  cznrng  45401  zrinitorngc  45446  zrtermorngc  45447  zrtermoringc  45516  coe1id  45613  blenre  45808  blennn  45809  2arymaptf  45886  itcoval1  45897  itcovalendof  45903  ehl2eudisval0  45959  eenglngeehlnmlem2  45972  itsclc0yqsol  45998  inlinecirc02plem  46020  ipolub  46162  ipoglb  46165