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 584	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  689  mpan2  691  biadanid  822  mpjaodan  960  mpjao3dan  1434  mpd3an3  1464  elabd2  3654  eueq2  3698  csbiegf  3912  difsnb  4787  reusv3i  5379  frpoinsg  6337  fimadmfo  6804  fimadmfoALT  6806  fvtresfn  6993  fvmpt3  6995  ffvelcdmd  7080  fnressn  7153  fsnex  7281  f1oiso2  7350  riota5f  7395  onsuc  7810  onsucuni  7827  frrlem10  8299  seqomlem2  8470  oaordi  8563  nnaordi  8635  qsdisj  8813  dom2lem  9011  canth2g  9150  limenpsi  9171  nnfi  9186  php4  9229  onfin  9244  sucxpdom  9268  xpfiOLD  9336  dmfi  9352  fiin  9439  supiso  9493  ordiso2  9534  wdom2d  9599  infeq5  9656  cantnfp1lem3  9699  cantnflem1d  9707  rankwflemb  9812  onenon  9968  cardonle  9976  sdomsdomcardi  9990  acni  10064  cardaleph  10108  djuen  10189  djuinf  10208  infdju1  10209  nnadju  10217  pwsdompw  10222  infdif  10227  cfval  10266  fin34  10409  fin1a2lem1  10419  fin1a2  10434  ttukeylem6  10533  sdomsdomcard  10579  canth3  10580  fpwwe2  10662  canthwelem  10669  gchdju1  10675  pwfseqlem4  10681  gchdjuidm  10687  gchxpidm  10688  tskwe2  10792  rankcf  10796  tskuni  10802  gruxp  10826  dmrecnq  10987  lterpq  10989  archnq  10999  reclem3pr  11068  reclem4pr  11069  0idsr  11116  lep1  12087  ledivp1  12149  negfi  12196  supaddc  12214  supmul1  12216  suprzcl  12678  uz11  12882  zmin  12965  zbtwnre  12967  rpnnen1lem4  13001  rpnnen1lem5  13002  xnegid  13259  supxrre  13348  infxrre  13358  eluzfz2  13554  fzsuc  13593  fzsuc2  13604  fzp1disj  13605  fzneuz  13630  nn0p1elfzo  13724  fllep1  13823  fraclt1  13824  fracle1  13825  fracge0  13826  flhalf  13852  ceige  13866  ceim1l  13869  fldiv  13882  modval  13893  suppssfz  14017  seqeq1  14027  expubnd  14201  iexpcyc  14230  binom2sub1  14244  faclbnd4lem3  14318  pfxid  14707  pfxccatpfx2  14760  swrdccat3blem  14762  cshw0  14817  cshwn  14820  cshimadifsn  14853  cshimadifsn0  14854  pfx2  14971  trclexlem  15018  shftfval  15094  shftcan1  15107  reval  15130  cjmulrcl  15168  addcj  15172  absval  15262  absneg  15301  abscj  15303  sqabsadd  15306  sqabssub  15307  leabs  15323  sqreulem  15383  lo1res  15580  o1of2  15634  o1rlimmul  15640  flo1  15875  trirecip  15884  efcan  16117  efi4p  16160  resin4p  16161  recos4p  16162  sincossq  16199  ruclem10  16262  iddvds  16294  1dvds  16295  2ebits  16471  lcmftp  16660  coprmgcdb  16673  1idssfct  16704  exprmfct  16728  eulerthlem2  16806  odzphi  16821  pcprendvds  16865  pcmpt  16917  oddprmdvds  16928  vdwlem8  17013  0ram2  17046  prmgaplem7  17082  setsn0fun  17197  setsexstruct2  17199  pwsvscaval  17514  2initoinv  18028  initoeu1  18029  initoeu2lem1  18032  initoeu2  18034  2termoinv  18035  termoeu1  18036  homarel  18054  joinfval  18388  meetfval  18402  latjcom  18462  latmcom  18478  0subm  18800  sgrp2nmndlem5  18912  grprcan  18961  isgrpid2  18964  grpinvid  18987  mulgnn0z  19089  0subgOLD  19140  qus0  19177  eqg0subg  19184  ghmker  19230  symgbasmap  19363  symginv  19388  pmtrfrn  19444  odmulg2  19541  slwpgp  19599  pj1eq  19686  efgtf  19708  frgpinv  19750  frgpup2  19762  cnaddablx  19854  cnaddabl  19855  zaddablx  19858  imasabl  19862  dprdfadd  20008  dpjidcl  20046  dpjlid  20049  pgpfac1lem3  20065  srgen1zr  20181  1unit  20339  unitgrpid  20350  1rinv  20360  irredn0  20388  irredneg  20395  c0snmgmhm  20427  rngisomring1  20433  zrrnghm  20501  rnrhmsubrg  20570  zrinitorngc  20607  zrtermorngc  20608  zrtermoringc  20640  isdrng2  20708  ringen1zr  20743  abv0  20788  abv1z  20789  abvneg  20791  lmodfopne  20862  lsssn0  20910  lspsn0  20970  lsp0  20971  lmhmvsca  21008  lmhmrnlss  21013  lmhmkerlss  21014  lsppratlem5  21117  rsp1  21203  kerlidl  21244  ring2idlqus  21275  rngqiprngfulem4  21280  rngqiprngfu  21283  cnfldneg  21363  zringcyg  21435  chrid  21491  chrrhm  21497  ip0r  21602  ocvlss  21637  ocv1  21644  rlmassa  21836  psrbagfsupp  21884  snifpsrbag  21885  psrbaglefi  21891  psrvscaval  21915  psrdi  21930  psrdir  21931  mplvscaval  21981  mhpmpl  22087  mhpdeg  22088  mhppwdeg  22093  psdmul  22109  psdpw  22113  coe1sclmulfv  22225  ply1idvr1OLD  22238  evl1var  22279  mamuvs1  22348  mamuvs2  22349  matecl  22368  matvscacell  22379  mat0scmat  22481  submaval0  22523  mdetrsca  22546  maduval  22581  minmar1val0  22590  pmatcollpw3fi1lem2  22730  chcoeffeqlem  22828  cayleyhamilton0  22832  cayleyhamiltonALT  22834  toponsspwpw  22865  cctop  22949  cldval  22966  ntrfval  22967  clsfval  22968  cmclsopn  23005  opncldf3  23029  neifval  23042  lpfval  23081  cnrmnrm  23304  dis2ndc  23403  islocfin  23460  tx1cn  23552  idqtop  23649  kqtopon  23670  kqid  23671  kqcld  23678  hmphen2  23742  filssufil  23855  ufileu  23862  alexsublem  23987  efmndtmd  24044  symgtgp  24049  ustuqtop4  24188  cstucnd  24227  metustexhalf  24500  nm0  24573  rlmnlm  24632  nmolb  24661  metdseq0  24799  pi1xfrval  25010  clmvneg1  25055  clmvsubval  25065  ipcau2  25191  tcphcphlem1  25192  tcphcphlem2  25193  cmetcaulem  25245  ovolicc2lem3  25477  ovolicc2lem4  25478  mbfmulc2lem  25605  i1fpos  25664  mbfi1fseqlem3  25675  itg2ge0  25693  bddiblnc  25800  dvres2  25870  dvaddbr  25897  dvmulbr  25898  dvmulbrOLD  25899  dvcobr  25906  dvcobrOLD  25907  dvfsumlem4  25993  ftc1a  26001  ftc1lem6  26005  uc1pmon1p  26114  ig1pval2  26139  dgradd2  26231  dgrcolem2  26237  plydivlem4  26261  plydiveu  26263  elqaalem3  26286  qaa  26288  ulmdvlem1  26366  abelthlem6  26403  abelthlem7  26405  eflogeq  26568  jensenlem2  26955  harmonicbnd4  26978  sgmnncl  27114  dchrptlem2  27233  1lgs  27308  lgs1  27309  2sqcoprm  27403  addsqnreup  27411  dchrisumlem2  27458  dchrisum0lem2a  27485  selberg2lem  27518  pntrsumo1  27533  pntrsumbnd  27534  pntpbnd1  27554  pntlemr  27570  pntlemj  27571  padicabvf  27599  bdayval  27617  noextendgt  27639  nosupbnd2lem1  27684  noinfbnd2lem1  27699  noetainflem4  27709  oldval  27819  divsmul  28180  divscl  28182  seqsp1  28262  zzs12  28396  remulscllem1  28408  incistruhgr  29063  subgrprop3  29260  subgruhgredgd  29268  usgrexi  29425  cusgrexi  29427  cusgrsizeinds  29437  vtxdgfusgrf  29482  1hevtxdg1  29491  1egrvtxdg1  29494  ewlkprop  29588  wlklenvm1  29607  wlkl1loop  29623  wlkp1lem4  29661  2pthnloop  29718  upgrclwlkcompim  29768  crctcshwlkn0lem4  29800  crctcshwlkn0lem5  29801  crctcshwlkn0lem6  29802  crctcshwlkn0lem7  29803  crctcshlem4  29807  wspthnonp  29846  wlkswwlksf1o  29866  wwlksnwwlksnon  29902  umgr2wlkon  29937  wwlks2onv  29940  elwwlks2ons3im  29941  elwspths2spth  29954  umgrclwwlkge2  29977  clwlkclwwlkf1lem3  29992  erclwwlkref  30006  clwwlknp  30023  wwlksext2clwwlk  30043  wwlksubclwwlk  30044  0pthon1  30114  1wlkdlem4  30126  1pthd  30129  3spthd  30162  eupth2eucrct  30203  eucrctshift  30229  eucrct2eupth  30231  frgrncvvdeqlem8  30292  frgr2wwlkeqm  30317  isgrpoi  30484  grpoinvfval  30508  grpodivfval  30520  vcz  30561  cnaddabloOLD  30567  nvz0  30654  sspz  30721  lno0  30742  nmobndi  30761  ipasslem2  30818  shunssi  31354  ococin  31394  ssjo  31433  pjocini  31684  nlfnval  31867  lncnopbd  32023  riesz3i  32048  cnlnadjlem7  32059  pjclem4  32185  pj3si  32193  hstoc  32208  hstnmoc  32209  hstoh  32218  hst0  32219  mdsl2i  32308  chirredlem3  32378  chirredlem4  32379  dmdbr5ati  32408  rexunirn  32478  fcnvgreu  32656  infxrge0glb  32747  sgnneg  32817  omndmul2  33085  omndmul  33087  cycpmco2lem5  33146  cycpmco2lem6  33147  cycpmco2lem7  33148  isarchi3  33190  orng0le1  33339  nsgqusf1olem2  33434  ssdifidllem  33476  ssmxidllem  33493  rprmdvdspow  33553  ressply1sub  33588  fedgmullem1  33674  extdg1id  33712  nn0constr  33800  zartopn  33911  zarcmplem  33917  esumcvg  34122  esumcvgre  34127  sigaval  34147  unelldsys  34194  fiunelros  34210  measval  34234  pmeasmono  34361  probfinmeasb  34465  ballotlemfc0  34530  ballotlemfcc  34531  ballotlemsi  34552  ballotlemfrci  34565  signlem0  34624  breprexp  34670  bnj1006  34996  bnj1110  35018  bnj1253  35053  bnj1280  35056  bnj1463  35091  bnj1312  35094  erdszelem7  35224  erdszelem8  35225  cvmliftlem10  35321  cvmliftlem13  35323  cvmlift2lem9  35338  cvmlift3lem6  35351  cvmlift3lem7  35352  cvmlift3lem9  35354  satfv1lem  35389  dfrdg2  35818  cldregopn  36354  tailfval  36395  filnetlem3  36403  filnetlem4  36404  ontopbas  36451  bj-elid4  37191  bj-imdiridlem  37208  f1omptsnlem  37359  icoreunrn  37382  relowlpssretop  37387  fvineqsnf1  37433  wl-sbal2  37587  unccur  37632  poimirlem1  37650  poimirlem2  37651  poimirlem4  37653  poimirlem6  37655  poimirlem7  37656  poimirlem11  37660  poimirlem12  37661  poimirlem17  37666  poimirlem20  37669  poimirlem22  37671  poimirlem23  37672  poimirlem28  37677  poimir  37682  ismblfin  37690  cnambfre  37697  ftc1cnnc  37721  dvasin  37733  ismtyres  37837  heiborlem8  37847  ghomidOLD  37918  rngosn6  37955  rngonegmn1l  37970  rngonegmn1r  37971  rngoneglmul  37972  rngonegrmul  37973  idlnegcl  38051  0idl  38054  0rngo  38056  smprngopr  38081  cossex  38442  qsdisjALTV  38638  cnvepresdmqss  38675  mpets2  38864  lkrval  39111  ldualvaddval  39154  ldualvsval  39161  opoc1  39225  pmap0  39789  pmap1N  39791  pexmidALTN  40002  cdleme31fv  40414  cdlemg27b  40720  erngdvlem4  41015  erng0g  41018  erngdvlem4-rN  41023  dvalveclem  41049  dvh0g  41135  dih0cnv  41307  dih1rn  41311  dih1cnv  41312  doch0  41382  doch1  41383  lcfl7lem  41523  mapdheq  41752  hdmap1eq  41825  hdmapval2lem  41855  hgmapvvlem3  41949  zndvdchrrhm  41990  lcmineqlem13  42059  aks4d1p9  42106  primrootsunit1  42115  aks6d1c1p1  42125  aks6d1c1p6  42132  aks6d1c1p8  42133  sticksstones1  42164  sticksstones6  42169  sticksstones7  42170  sticksstones11  42174  sticksstones12a  42175  sticksstones12  42176  sticksstones22  42186  aks6d1c6isolem1  42192  aks6d1c6isolem2  42193  unitscyglem5  42217  renegid  42391  sn-0ne2  42424  remul01  42425  remulinvcom  42450  sn-0tie0  42457  renegmulnnass  42471  sn-inelr  42485  domnexpgn0cl  42521  abvexp  42530  frlmsnic  42538  fsuppssind  42591  mzpval  42730  mzpindd  42744  pellex  42833  2nn0ind  42944  jm2.26lem3  43000  pw2f1o2val  43038  wepwsolem  43041  fnwe2lem3  43051  lnmfg  43081  dgrsub2  43134  mpaaeu  43149  flcidc  43169  dflim5  43328  naddwordnexlem1  43396  rtrclexlem  43615  cnvrcl0  43624  brcoffn  44029  clsk1indlem3  44042  clsneif1o  44103  clsneicnv  44104  clsneikex  44105  clsneinex  44106  neicvgmex  44116  neicvgel1  44118  suprleubrd  44165  suprlubrd  44167  imo72b2  44171  dvconstbi  44333  bcc0  44339  binomcxplemnotnn0  44355  nnfoctb  45052  infleinflem1  45377  fprodcnlem  45608  sumnnodd  45639  icccncfext  45896  itgsin0pilem1  45959  stoweidlem32  46041  stoweidlem35  46044  stoweidlem36  46045  stoweidlem37  46046  stoweidlem43  46052  stoweidlem50  46059  wallispilem5  46078  stirlinglem2  46084  stirlinglem3  46085  stirlinglem4  46086  stirlinglem8  46090  stirlinglem11  46093  stirlinglem12  46094  stirlinglem14  46096  stirlinglem15  46097  fourierdlem11  46127  fourierdlem20  46136  fourierdlem21  46137  fourierdlem41  46157  fourierdlem42  46158  fourierdlem48  46163  fourierdlem49  46164  fourierdlem64  46179  fourierdlem71  46186  fourierdlem79  46194  fourierdlem90  46205  fourierdlem91  46206  fourierswlem  46239  etransclem17  46260  etransclem38  46281  saluni  46334  meaiininclem  46495  issmflelem  46753  issmfgtlem  46764  issmfgelem  46778  smflimsuplem4  46832  f1cof1blem  47083  zplusmodne  47352  m1modne  47357  submodneaddmod  47360  sprval  47473  prprval  47508  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbnd  47803  isubgrvtxuhgr  47857  isubgredg  47859  grimcnv  47881  isuspgrim  47889  gricushgr  47910  uhgrimisgrgric  47924  grtriclwlk3  47937  isubgr3stgrlem7  47964  grlimgrtri  47988  grlictr  48000  gpgvtx0  48037  gpgvtx1  48038  gpgprismgrusgra  48042  gpgedgvtx1  48046  gpg3kgrtriex  48071  isclintop  48162  clintopcllaw  48166  nzrneg1ne0  48185  lidldomn1  48186  zlidlring  48189  uzlidlring  48190  2zrngnmlid  48210  cznrng  48216  coe1id  48340  blenre  48534  blennn  48535  2arymaptf  48612  itcoval1  48623  itcovalendof  48629  ehl2eudisval0  48685  eenglngeehlnmlem2  48698  itsclc0yqsol  48724  inlinecirc02plem  48746  ipolub  48942  ipoglb  48945  nelsubclem  49014  imaid  49074  imaf1co  49075  setrec2mpt  49541