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

This theorem is referenced by:  mpidan  688  mpan2  690  biadanid  822  mpjaodan  959  mpjao3dan  1432  mpd3an3  1462  elabd2  3683  eueq2  3732  csbiegf  3955  difsnb  4831  reusv3i  5422  frpoinsg  6375  fimadmfo  6843  fimadmfoALT  6845  fvtresfn  7031  fvmpt3  7033  ffvelcdmd  7119  fnressn  7192  fsnex  7319  f1oiso2  7388  riota5f  7433  onsuc  7847  onsucuni  7864  frrlem10  8336  seqomlem2  8507  oaordi  8602  nnaordi  8674  qsdisj  8852  dom2lem  9052  canth2g  9197  limenpsi  9218  nnfi  9233  php4  9276  onfin  9293  sucxpdom  9318  xpfiOLD  9387  dmfi  9403  pwfilemOLD  9416  pwfiOLD  9417  fiin  9491  supiso  9544  ordiso2  9584  wdom2d  9649  infeq5  9706  cantnfp1lem3  9749  cantnflem1d  9757  rankwflemb  9862  onenon  10018  cardonle  10026  sdomsdomcardi  10040  acni  10114  cardaleph  10158  djuen  10239  djuinf  10258  infdju1  10259  nnadju  10267  pwsdompw  10272  infdif  10277  cfval  10316  fin34  10459  fin1a2lem1  10469  fin1a2  10484  ttukeylem6  10583  sdomsdomcard  10629  canth3  10630  fpwwe2  10712  canthwelem  10719  gchdju1  10725  pwfseqlem4  10731  gchdjuidm  10737  gchxpidm  10738  tskwe2  10842  rankcf  10846  tskuni  10852  gruxp  10876  dmrecnq  11037  lterpq  11039  archnq  11049  reclem3pr  11118  reclem4pr  11119  0idsr  11166  lep1  12135  ledivp1  12197  negfi  12244  supaddc  12262  supmul1  12264  suprzcl  12723  uz11  12928  zmin  13009  zbtwnre  13011  rpnnen1lem4  13045  rpnnen1lem5  13046  xnegid  13300  supxrre  13389  infxrre  13398  eluzfz2  13592  fzsuc  13631  fzsuc2  13642  fzp1disj  13643  fzneuz  13665  nn0p1elfzo  13759  fllep1  13852  fraclt1  13853  fracle1  13854  fracge0  13855  flhalf  13881  ceige  13895  ceim1l  13898  fldiv  13911  modval  13922  suppssfz  14045  seqeq1  14055  expubnd  14227  iexpcyc  14256  binom2sub1  14270  faclbnd4lem3  14344  pfxid  14732  pfxccatpfx2  14785  swrdccat3blem  14787  cshw0  14842  cshwn  14845  cshimadifsn  14878  cshimadifsn0  14879  pfx2  14996  trclexlem  15043  shftfval  15119  shftcan1  15132  reval  15155  cjmulrcl  15193  addcj  15197  absval  15287  absneg  15326  abscj  15328  sqabsadd  15331  sqabssub  15332  leabs  15348  sqreulem  15408  lo1res  15605  o1of2  15659  o1rlimmul  15665  flo1  15902  trirecip  15911  efcan  16144  efi4p  16185  resin4p  16186  recos4p  16187  sincossq  16224  ruclem10  16287  iddvds  16318  1dvds  16319  2ebits  16493  lcmftp  16683  coprmgcdb  16696  1idssfct  16727  exprmfct  16751  eulerthlem2  16829  odzphi  16843  pcprendvds  16887  pcmpt  16939  oddprmdvds  16950  vdwlem8  17035  0ram2  17068  prmgaplem7  17104  setsn0fun  17220  setsexstruct2  17222  pwsvscaval  17555  2initoinv  18077  initoeu1  18078  initoeu2lem1  18081  initoeu2  18083  2termoinv  18084  termoeu1  18085  homarel  18103  joinfval  18443  meetfval  18457  latjcom  18517  latmcom  18533  0subm  18852  sgrp2nmndlem5  18964  grprcan  19013  isgrpid2  19016  grpinvid  19039  mulgnn0z  19141  0subgOLD  19192  qus0  19229  eqg0subg  19236  ghmker  19282  symgbasmap  19418  symginv  19444  pmtrfrn  19500  odmulg2  19597  slwpgp  19655  pj1eq  19742  efgtf  19764  frgpinv  19806  frgpup2  19818  cnaddablx  19910  cnaddabl  19911  zaddablx  19914  imasabl  19918  dprdfadd  20064  dpjidcl  20102  dpjlid  20105  pgpfac1lem3  20121  srgen1zr  20243  1unit  20400  unitgrpid  20411  1rinv  20421  irredn0  20449  irredneg  20456  c0snmgmhm  20488  rngisomring1  20494  zrrnghm  20562  rnrhmsubrg  20633  zrinitorngc  20664  zrtermorngc  20665  zrtermoringc  20697  isdrng2  20765  ringen1zr  20801  abv0  20846  abv1z  20847  abvneg  20849  lmodfopne  20920  lsssn0  20969  lspsn0  21029  lsp0  21030  lmhmvsca  21067  lmhmrnlss  21072  lmhmkerlss  21073  lsppratlem5  21176  rsp1  21270  kerlidl  21311  ring2idlqus  21342  rngqiprngfulem4  21347  rngqiprngfu  21350  cnfldneg  21431  zringcyg  21503  chrid  21563  chrrhm  21569  ip0r  21678  ocvlss  21713  ocv1  21720  rlmassa  21914  psrbagfsupp  21962  snifpsrbag  21963  psrbaglefi  21969  psrvscaval  21993  psrdi  22008  psrdir  22009  mplvscaval  22059  mhpmpl  22171  mhpdeg  22172  mhppwdeg  22177  psdmul  22193  coe1sclmulfv  22307  ply1idvr1OLD  22320  evl1var  22361  mamuvs1  22430  mamuvs2  22431  matecl  22452  matvscacell  22463  mat0scmat  22565  submaval0  22607  mdetrsca  22630  maduval  22665  minmar1val0  22674  pmatcollpw3fi1lem2  22814  chcoeffeqlem  22912  cayleyhamilton0  22916  cayleyhamiltonALT  22918  toponsspwpw  22949  cctop  23034  cldval  23052  ntrfval  23053  clsfval  23054  cmclsopn  23091  opncldf3  23115  neifval  23128  lpfval  23167  cnrmnrm  23390  dis2ndc  23489  islocfin  23546  tx1cn  23638  idqtop  23735  kqtopon  23756  kqid  23757  kqcld  23764  hmphen2  23828  filssufil  23941  ufileu  23948  alexsublem  24073  efmndtmd  24130  symgtgp  24135  ustuqtop4  24274  cstucnd  24314  metustexhalf  24590  nm0  24663  rlmnlm  24730  nmolb  24759  metdseq0  24895  pi1xfrval  25106  clmvneg1  25151  clmvsubval  25161  ipcau2  25287  tcphcphlem1  25288  tcphcphlem2  25289  cmetcaulem  25341  ovolicc2lem3  25573  ovolicc2lem4  25574  mbfmulc2lem  25701  i1fpos  25761  mbfi1fseqlem3  25772  itg2ge0  25790  bddiblnc  25897  dvres2  25967  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcobr  26003  dvcobrOLD  26004  dvfsumlem4  26090  ftc1a  26098  ftc1lem6  26102  uc1pmon1p  26211  ig1pval2  26236  dgradd2  26328  dgrcolem2  26334  plydivlem4  26356  plydiveu  26358  elqaalem3  26381  qaa  26383  ulmdvlem1  26461  abelthlem6  26498  abelthlem7  26500  eflogeq  26662  jensenlem2  27049  harmonicbnd4  27072  sgmnncl  27208  dchrptlem2  27327  1lgs  27402  lgs1  27403  2sqcoprm  27497  addsqnreup  27505  dchrisumlem2  27552  dchrisum0lem2a  27579  selberg2lem  27612  pntrsumo1  27627  pntrsumbnd  27628  pntpbnd1  27648  pntlemr  27664  pntlemj  27665  padicabvf  27693  bdayval  27711  noextendgt  27733  nosupbnd2lem1  27778  noinfbnd2lem1  27793  noetainflem4  27803  oldval  27911  divsmul  28263  divscl  28265  seqsp1  28335  zzs12  28441  remulscllem1  28450  incistruhgr  29114  subgrprop3  29311  subgruhgredgd  29319  usgrexi  29476  cusgrexi  29478  cusgrsizeinds  29488  vtxdgfusgrf  29533  1hevtxdg1  29542  1egrvtxdg1  29545  ewlkprop  29639  wlklenvm1  29658  wlkl1loop  29674  wlkp1lem4  29712  2pthnloop  29767  upgrclwlkcompim  29817  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshwlkn0lem6  29848  crctcshwlkn0lem7  29849  crctcshlem4  29853  wspthnonp  29892  wlkswwlksf1o  29912  wwlksnwwlksnon  29948  umgr2wlkon  29983  wwlks2onv  29986  elwwlks2ons3im  29987  elwspths2spth  30000  umgrclwwlkge2  30023  clwlkclwwlkf1lem3  30038  erclwwlkref  30052  clwwlknp  30069  wwlksext2clwwlk  30089  wwlksubclwwlk  30090  0pthon1  30160  1wlkdlem4  30172  1pthd  30175  3spthd  30208  eupth2eucrct  30249  eucrctshift  30275  eucrct2eupth  30277  frgrncvvdeqlem8  30338  frgr2wwlkeqm  30363  isgrpoi  30530  grpoinvfval  30554  grpodivfval  30566  vcz  30607  cnaddabloOLD  30613  nvz0  30700  sspz  30767  lno0  30788  nmobndi  30807  ipasslem2  30864  shunssi  31400  ococin  31440  ssjo  31479  pjocini  31730  nlfnval  31913  lncnopbd  32069  riesz3i  32094  cnlnadjlem7  32105  pjclem4  32231  pj3si  32239  hstoc  32254  hstnmoc  32255  hstoh  32264  hst0  32265  mdsl2i  32354  chirredlem3  32424  chirredlem4  32425  dmdbr5ati  32454  rexunirn  32520  fcnvgreu  32691  infxrge0glb  32772  omndmul2  33062  omndmul  33064  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  isarchi3  33167  orng0le1  33307  nsgqusf1olem2  33407  ssdifidllem  33449  ssmxidllem  33466  rprmdvdspow  33526  ressply1sub  33560  fedgmullem1  33642  extdg1id  33676  zartopn  33821  zarcmplem  33827  esumcvg  34050  esumcvgre  34055  sigaval  34075  unelldsys  34122  fiunelros  34138  measval  34162  pmeasmono  34289  probfinmeasb  34393  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemsi  34479  ballotlemfrci  34492  sgnneg  34505  signlem0  34564  breprexp  34610  bnj1006  34936  bnj1110  34958  bnj1253  34993  bnj1280  34996  bnj1463  35031  bnj1312  35034  erdszelem7  35165  erdszelem8  35166  cvmliftlem10  35262  cvmliftlem13  35264  cvmlift2lem9  35279  cvmlift3lem6  35292  cvmlift3lem7  35293  cvmlift3lem9  35295  satfv1lem  35330  dfrdg2  35759  cldregopn  36297  tailfval  36338  filnetlem3  36346  filnetlem4  36347  ontopbas  36394  bj-elid4  37134  bj-imdiridlem  37151  f1omptsnlem  37302  icoreunrn  37325  relowlpssretop  37330  fvineqsnf1  37376  wl-sbal2  37518  unccur  37563  poimirlem1  37581  poimirlem2  37582  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem11  37591  poimirlem12  37592  poimirlem17  37597  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimirlem28  37608  poimir  37613  ismblfin  37621  cnambfre  37628  ftc1cnnc  37652  dvasin  37664  ismtyres  37768  heiborlem8  37778  ghomidOLD  37849  rngosn6  37886  rngonegmn1l  37901  rngonegmn1r  37902  rngoneglmul  37903  rngonegrmul  37904  idlnegcl  37982  0idl  37985  0rngo  37987  smprngopr  38012  cossex  38375  qsdisjALTV  38571  cnvepresdmqss  38608  mpets2  38797  lkrval  39044  ldualvaddval  39087  ldualvsval  39094  opoc1  39158  pmap0  39722  pmap1N  39724  pexmidALTN  39935  cdleme31fv  40347  cdlemg27b  40653  erngdvlem4  40948  erng0g  40951  erngdvlem4-rN  40956  dvalveclem  40982  dvh0g  41068  dih0cnv  41240  dih1rn  41244  dih1cnv  41245  doch0  41315  doch1  41316  lcfl7lem  41456  mapdheq  41685  hdmap1eq  41758  hdmapval2lem  41788  hgmapvvlem3  41882  zndvdchrrhm  41927  lcmineqlem13  41998  aks4d1p9  42045  primrootsunit1  42054  aks6d1c1p1  42064  aks6d1c1p6  42071  aks6d1c1p8  42072  sticksstones1  42103  sticksstones6  42108  sticksstones7  42109  sticksstones11  42113  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  unitscyglem5  42156  renegid  42349  sn-0ne2  42382  remul01  42383  remulinvcom  42408  sn-0tie0  42415  renegmulnnass  42429  sn-inelr  42443  domnexpgn0cl  42478  abvexp  42487  frlmsnic  42495  fsuppssind  42548  mzpval  42688  mzpindd  42702  pellex  42791  2nn0ind  42902  jm2.26lem3  42958  pw2f1o2val  42996  wepwsolem  42999  fnwe2lem3  43009  lnmfg  43039  dgrsub2  43092  mpaaeu  43107  flcidc  43131  dflim5  43291  naddwordnexlem1  43359  rtrclexlem  43578  cnvrcl0  43587  brcoffn  43992  clsk1indlem3  44005  clsneif1o  44066  clsneicnv  44067  clsneikex  44068  clsneinex  44069  neicvgmex  44079  neicvgel1  44081  suprleubrd  44128  suprlubrd  44130  imo72b2  44134  dvconstbi  44303  bcc0  44309  binomcxplemnotnn0  44325  nnfoctb  44949  infleinflem1  45285  fprodcnlem  45520  sumnnodd  45551  icccncfext  45808  itgsin0pilem1  45871  stoweidlem32  45953  stoweidlem35  45956  stoweidlem36  45957  stoweidlem37  45958  stoweidlem43  45964  stoweidlem50  45971  wallispilem5  45990  stirlinglem2  45996  stirlinglem3  45997  stirlinglem4  45998  stirlinglem8  46002  stirlinglem11  46005  stirlinglem12  46006  stirlinglem14  46008  stirlinglem15  46009  fourierdlem11  46039  fourierdlem20  46048  fourierdlem21  46049  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem64  46091  fourierdlem71  46098  fourierdlem79  46106  fourierdlem90  46117  fourierdlem91  46118  fourierswlem  46151  etransclem17  46172  etransclem38  46193  saluni  46246  meaiininclem  46407  issmflelem  46665  issmfgtlem  46676  issmfgelem  46690  smflimsuplem4  46744  f1cof1blem  46989  sprval  47353  prprval  47388  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbnd  47683  isubgrvtxuhgr  47736  isuspgrim  47759  grimcnv  47763  gricushgr  47770  uhgrimisgrgric  47783  grtriclwlk3  47796  grlimgrtri  47820  grlictr  47832  isclintop  47930  clintopcllaw  47934  nzrneg1ne0  47953  lidldomn1  47954  zlidlring  47957  uzlidlring  47958  2zrngnmlid  47978  cznrng  47984  coe1id  48113  blenre  48308  blennn  48309  2arymaptf  48386  itcoval1  48397  itcovalendof  48403  ehl2eudisval0  48459  eenglngeehlnmlem2  48472  itsclc0yqsol  48498  inlinecirc02plem  48520  ipolub  48660  ipoglb  48663  setrec2mpt  48789