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  3623  eueq2  3667  csbiegf  3881  difsnb  4756  reusv3i  5340  frpoinsg  6286  fimadmfo  6740  fimadmfoALT  6742  fvtresfn  6926  fvmpt3  6928  ffvelcdmd  7013  fnressn  7086  fsnex  7212  f1oiso2  7281  riota5f  7326  onsuc  7738  onsucuni  7753  frrlem10  8220  seqomlem2  8365  oaordi  8456  nnaordi  8528  qsdisj  8713  dom2lem  8909  canth2g  9039  limenpsi  9060  nnfi  9072  php4  9114  onfin  9119  sucxpdom  9140  dmfi  9214  fiin  9301  supiso  9355  ordiso2  9396  wdom2d  9461  elirrv  9478  infeq5  9522  cantnfp1lem3  9565  cantnflem1d  9573  rankwflemb  9678  onenon  9834  cardonle  9842  sdomsdomcardi  9856  acni  9928  cardaleph  9972  djuen  10053  djuinf  10072  infdju1  10073  nnadju  10081  pwsdompw  10086  infdif  10091  cfval  10130  fin34  10273  fin1a2lem1  10283  fin1a2  10298  ttukeylem6  10397  sdomsdomcard  10443  canth3  10444  fpwwe2  10526  canthwelem  10533  gchdju1  10539  pwfseqlem4  10545  gchdjuidm  10551  gchxpidm  10552  tskwe2  10656  rankcf  10660  tskuni  10666  gruxp  10690  dmrecnq  10851  lterpq  10853  archnq  10863  reclem3pr  10932  reclem4pr  10933  0idsr  10980  lep1  11954  ledivp1  12016  negfi  12063  supaddc  12081  supmul1  12083  suprzcl  12545  uz11  12749  zmin  12834  zbtwnre  12836  rpnnen1lem4  12870  rpnnen1lem5  12871  xnegid  13129  supxrre  13218  infxrre  13228  eluzfz2  13424  fzsuc  13463  fzsuc2  13474  fzp1disj  13475  fzneuz  13500  nn0p1elfzo  13594  fllep1  13697  fraclt1  13698  fracle1  13699  fracge0  13700  flhalf  13726  ceige  13740  ceim1l  13743  fldiv  13756  modval  13767  suppssfz  13893  seqeq1  13903  expubnd  14077  iexpcyc  14106  binom2sub1  14120  faclbnd4lem3  14194  pfxid  14584  pfxccatpfx2  14636  swrdccat3blem  14638  cshw0  14693  cshwn  14696  cshimadifsn  14728  cshimadifsn0  14729  pfx2  14846  trclexlem  14893  shftfval  14969  shftcan1  14982  reval  15005  cjmulrcl  15043  addcj  15047  absval  15137  absneg  15176  abscj  15178  sqabsadd  15181  sqabssub  15182  leabs  15198  sqreulem  15259  lo1res  15458  o1of2  15512  o1rlimmul  15518  flo1  15753  trirecip  15762  efcan  15995  efi4p  16038  resin4p  16039  recos4p  16040  sincossq  16077  ruclem10  16140  iddvds  16172  1dvds  16173  2ebits  16350  lcmftp  16539  coprmgcdb  16552  1idssfct  16583  exprmfct  16607  eulerthlem2  16685  odzphi  16700  pcprendvds  16744  pcmpt  16796  oddprmdvds  16807  vdwlem8  16892  0ram2  16925  prmgaplem7  16961  setsn0fun  17076  setsexstruct2  17078  pwsvscaval  17391  2initoinv  17909  initoeu1  17910  initoeu2lem1  17913  initoeu2  17915  2termoinv  17916  termoeu1  17917  homarel  17935  joinfval  18269  meetfval  18283  latjcom  18345  latmcom  18361  0subm  18717  sgrp2nmndlem5  18829  grprcan  18878  isgrpid2  18881  grpinvid  18904  mulgnn0z  19006  0subgOLD  19057  qus0  19094  eqg0subg  19101  ghmker  19147  symgbasmap  19282  symginv  19307  pmtrfrn  19363  odmulg2  19460  slwpgp  19518  pj1eq  19605  efgtf  19627  frgpinv  19669  frgpup2  19681  cnaddablx  19773  cnaddabl  19774  zaddablx  19777  imasabl  19781  dprdfadd  19927  dpjidcl  19965  dpjlid  19968  pgpfac1lem3  19984  omndmul2  20038  omndmul  20040  srgen1zr  20127  1unit  20285  unitgrpid  20296  1rinv  20306  irredn0  20334  irredneg  20341  c0snmgmhm  20373  rngisomring1  20379  zrrnghm  20444  rnrhmsubrg  20513  zrinitorngc  20550  zrtermorngc  20551  zrtermoringc  20583  isdrng2  20651  ringen1zr  20686  abv0  20731  abv1z  20732  abvneg  20734  orng0le1  20782  lmodfopne  20826  lsssn0  20874  lspsn0  20934  lsp0  20935  lmhmvsca  20972  lmhmrnlss  20977  lmhmkerlss  20978  lsppratlem5  21081  rsp1  21167  kerlidl  21208  ring2idlqus  21239  rngqiprngfulem4  21244  rngqiprngfu  21247  cnfldneg  21325  zringcyg  21399  chrid  21455  chrrhm  21461  ip0r  21567  ocvlss  21602  ocv1  21609  rlmassa  21801  psrbagfsupp  21849  snifpsrbag  21850  psrbaglefi  21856  psrvscaval  21880  psrdi  21895  psrdir  21896  mplvscaval  21946  mhpmpl  22052  mhpdeg  22053  mhppwdeg  22058  psdmul  22074  psdpw  22078  coe1sclmulfv  22190  ply1idvr1OLD  22203  evl1var  22244  mamuvs1  22313  mamuvs2  22314  matecl  22333  matvscacell  22344  mat0scmat  22446  submaval0  22488  mdetrsca  22511  maduval  22546  minmar1val0  22555  pmatcollpw3fi1lem2  22695  chcoeffeqlem  22793  cayleyhamilton0  22797  cayleyhamiltonALT  22799  toponsspwpw  22830  cctop  22914  cldval  22931  ntrfval  22932  clsfval  22933  cmclsopn  22970  opncldf3  22994  neifval  23007  lpfval  23046  cnrmnrm  23269  dis2ndc  23368  islocfin  23425  tx1cn  23517  idqtop  23614  kqtopon  23635  kqid  23636  kqcld  23643  hmphen2  23707  filssufil  23820  ufileu  23827  alexsublem  23952  efmndtmd  24009  symgtgp  24014  ustuqtop4  24152  cstucnd  24191  metustexhalf  24464  nm0  24537  rlmnlm  24596  nmolb  24625  metdseq0  24763  pi1xfrval  24974  clmvneg1  25019  clmvsubval  25029  ipcau2  25154  tcphcphlem1  25155  tcphcphlem2  25156  cmetcaulem  25208  ovolicc2lem3  25440  ovolicc2lem4  25441  mbfmulc2lem  25568  i1fpos  25627  mbfi1fseqlem3  25638  itg2ge0  25656  bddiblnc  25763  dvres2  25833  dvaddbr  25860  dvmulbr  25861  dvmulbrOLD  25862  dvcobr  25869  dvcobrOLD  25870  dvfsumlem4  25956  ftc1a  25964  ftc1lem6  25968  uc1pmon1p  26077  ig1pval2  26102  dgradd2  26194  dgrcolem2  26200  plydivlem4  26224  plydiveu  26226  elqaalem3  26249  qaa  26251  ulmdvlem1  26329  abelthlem6  26366  abelthlem7  26368  eflogeq  26531  jensenlem2  26918  harmonicbnd4  26941  sgmnncl  27077  dchrptlem2  27196  1lgs  27271  lgs1  27272  2sqcoprm  27366  addsqnreup  27374  dchrisumlem2  27421  dchrisum0lem2a  27448  selberg2lem  27481  pntrsumo1  27496  pntrsumbnd  27497  pntpbnd1  27517  pntlemr  27533  pntlemj  27534  padicabvf  27562  bdayval  27580  noextendgt  27602  nosupbnd2lem1  27647  noinfbnd2lem1  27662  noetainflem4  27672  oldval  27788  divsmul  28152  divscl  28154  seqsp1  28234  zzs12  28378  remulscllem1  28395  incistruhgr  29050  subgrprop3  29247  subgruhgredgd  29255  usgrexi  29412  cusgrexi  29414  cusgrsizeinds  29424  vtxdgfusgrf  29469  1hevtxdg1  29478  1egrvtxdg1  29481  ewlkprop  29575  wlklenvm1  29593  wlkl1loop  29609  wlkp1lem4  29646  2pthnloop  29702  upgrclwlkcompim  29752  crctcshwlkn0lem4  29784  crctcshwlkn0lem5  29785  crctcshwlkn0lem6  29786  crctcshwlkn0lem7  29787  crctcshlem4  29791  wspthnonp  29830  wlkswwlksf1o  29850  wwlksnwwlksnon  29886  umgr2wlkon  29921  wwlks2onv  29924  elwwlks2ons3im  29925  elwspths2spth  29938  umgrclwwlkge2  29961  clwlkclwwlkf1lem3  29976  erclwwlkref  29990  clwwlknp  30007  wwlksext2clwwlk  30027  wwlksubclwwlk  30028  0pthon1  30098  1wlkdlem4  30110  1pthd  30113  3spthd  30146  eupth2eucrct  30187  eucrctshift  30213  eucrct2eupth  30215  frgrncvvdeqlem8  30276  frgr2wwlkeqm  30301  isgrpoi  30468  grpoinvfval  30492  grpodivfval  30504  vcz  30545  cnaddabloOLD  30551  nvz0  30638  sspz  30705  lno0  30726  nmobndi  30745  ipasslem2  30802  shunssi  31338  ococin  31378  ssjo  31417  pjocini  31668  nlfnval  31851  lncnopbd  32007  riesz3i  32032  cnlnadjlem7  32043  pjclem4  32169  pj3si  32177  hstoc  32192  hstnmoc  32193  hstoh  32202  hst0  32203  mdsl2i  32292  chirredlem3  32362  chirredlem4  32363  dmdbr5ati  32392  rexunirn  32461  fcnvgreu  32645  infxrge0glb  32738  sgnneg  32806  cycpmco2lem5  33089  cycpmco2lem6  33090  cycpmco2lem7  33091  isarchi3  33146  nsgqusf1olem2  33369  ssdifidllem  33411  ssmxidllem  33428  rprmdvdspow  33488  ressply1sub  33523  fedgmullem1  33632  extdg1id  33669  nn0constr  33764  zartopn  33878  zarcmplem  33884  esumcvg  34089  esumcvgre  34094  sigaval  34114  unelldsys  34161  fiunelros  34177  measval  34201  pmeasmono  34327  probfinmeasb  34431  ballotlemfc0  34496  ballotlemfcc  34497  ballotlemsi  34518  ballotlemfrci  34531  signlem0  34590  breprexp  34636  bnj1006  34962  bnj1110  34984  bnj1253  35019  bnj1280  35022  bnj1463  35057  bnj1312  35060  erdszelem7  35209  erdszelem8  35210  cvmliftlem10  35306  cvmliftlem13  35308  cvmlift2lem9  35323  cvmlift3lem6  35336  cvmlift3lem7  35337  cvmlift3lem9  35339  satfv1lem  35374  dfrdg2  35808  cldregopn  36344  tailfval  36385  filnetlem3  36393  filnetlem4  36394  ontopbas  36441  bj-elid4  37181  bj-imdiridlem  37198  f1omptsnlem  37349  icoreunrn  37372  relowlpssretop  37377  fvineqsnf1  37423  wl-sbal2  37577  unccur  37622  poimirlem1  37640  poimirlem2  37641  poimirlem4  37643  poimirlem6  37645  poimirlem7  37646  poimirlem11  37650  poimirlem12  37651  poimirlem17  37656  poimirlem20  37659  poimirlem22  37661  poimirlem23  37662  poimirlem28  37667  poimir  37672  ismblfin  37680  cnambfre  37687  ftc1cnnc  37711  dvasin  37723  ismtyres  37827  heiborlem8  37837  ghomidOLD  37908  rngosn6  37945  rngonegmn1l  37960  rngonegmn1r  37961  rngoneglmul  37962  rngonegrmul  37963  idlnegcl  38041  0idl  38044  0rngo  38046  smprngopr  38071  cossex  38435  qsdisjALTV  38631  cnvepresdmqss  38669  mpets2  38858  lkrval  39106  ldualvaddval  39149  ldualvsval  39156  opoc1  39220  pmap0  39783  pmap1N  39785  pexmidALTN  39996  cdleme31fv  40408  cdlemg27b  40714  erngdvlem4  41009  erng0g  41012  erngdvlem4-rN  41017  dvalveclem  41043  dvh0g  41129  dih0cnv  41301  dih1rn  41305  dih1cnv  41306  doch0  41376  doch1  41377  lcfl7lem  41517  mapdheq  41746  hdmap1eq  41819  hdmapval2lem  41849  hgmapvvlem3  41943  zndvdchrrhm  41984  lcmineqlem13  42053  aks4d1p9  42100  primrootsunit1  42109  aks6d1c1p1  42119  aks6d1c1p6  42126  aks6d1c1p8  42127  sticksstones1  42158  sticksstones6  42163  sticksstones7  42164  sticksstones11  42168  sticksstones12a  42169  sticksstones12  42170  sticksstones22  42180  aks6d1c6isolem1  42186  aks6d1c6isolem2  42187  unitscyglem5  42211  renegid  42385  sn-0ne2  42418  remul01  42419  remulinvcom  42445  sn-0tie0  42463  renegmulnnass  42477  domnexpgn0cl  42535  abvexp  42544  frlmsnic  42552  fsuppssind  42605  mzpval  42744  mzpindd  42758  pellex  42847  2nn0ind  42957  jm2.26lem3  43013  pw2f1o2val  43051  wepwsolem  43054  fnwe2lem3  43064  lnmfg  43094  dgrsub2  43147  mpaaeu  43162  flcidc  43182  dflim5  43341  naddwordnexlem1  43409  rtrclexlem  43628  cnvrcl0  43637  brcoffn  44042  clsk1indlem3  44055  clsneif1o  44116  clsneicnv  44117  clsneikex  44118  clsneinex  44119  neicvgmex  44129  neicvgel1  44131  suprleubrd  44178  suprlubrd  44180  imo72b2  44184  dvconstbi  44346  bcc0  44352  binomcxplemnotnn0  44368  nnfoctb  45064  infleinflem1  45387  fprodcnlem  45618  sumnnodd  45649  icccncfext  45904  itgsin0pilem1  45967  stoweidlem32  46049  stoweidlem35  46052  stoweidlem36  46053  stoweidlem37  46054  stoweidlem43  46060  stoweidlem50  46067  wallispilem5  46086  stirlinglem2  46092  stirlinglem3  46093  stirlinglem4  46094  stirlinglem8  46098  stirlinglem11  46101  stirlinglem12  46102  stirlinglem14  46104  stirlinglem15  46105  fourierdlem11  46135  fourierdlem20  46144  fourierdlem21  46145  fourierdlem41  46165  fourierdlem42  46166  fourierdlem48  46171  fourierdlem49  46172  fourierdlem64  46187  fourierdlem71  46194  fourierdlem79  46202  fourierdlem90  46213  fourierdlem91  46214  fourierswlem  46247  etransclem17  46268  etransclem38  46289  saluni  46342  meaiininclem  46503  issmflelem  46761  issmfgtlem  46772  issmfgelem  46786  smflimsuplem4  46840  f1cof1blem  47084  zplusmodne  47353  m1modne  47358  submodneaddmod  47361  sprval  47489  prprval  47524  bgoldbtbndlem2  47816  bgoldbtbndlem3  47817  bgoldbtbnd  47819  isubgrvtxuhgr  47874  isubgredg  47876  grimcnv  47898  isuspgrim  47906  gricushgr  47927  uhgrimisgrgric  47941  grtriclwlk3  47955  isubgr3stgrlem7  47982  grlimgrtri  48013  grlictr  48025  gpgvtx0  48063  gpgvtx1  48064  gpgprismgrusgra  48068  gpgedgvtx1  48072  gpg3kgrtriex  48099  pgnbgreunbgrlem3  48128  pgnbgreunbgrlem6  48134  isclintop  48217  clintopcllaw  48221  nzrneg1ne0  48240  lidldomn1  48241  zlidlring  48244  uzlidlring  48245  2zrngnmlid  48265  cznrng  48271  coe1id  48395  blenre  48585  blennn  48586  2arymaptf  48663  itcoval1  48674  itcovalendof  48680  ehl2eudisval0  48736  eenglngeehlnmlem2  48749  itsclc0yqsol  48775  inlinecirc02plem  48797  ipolub  48998  ipoglb  49001  nelsubclem  49078  imaid  49165  imaf1co  49166  uptri  49225  uptrar  49227  uptrai  49228  oppc1stflem  49298  setrec2mpt  49708