Theorem mpdan 688

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 585	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  690  mpan2  692  biadanid  823  mpjaodan  961  mpjao3dan  1435  mpd3an3  1465  elabd2  3613  eueq2  3657  csbiegf  3871  difsnb  4752  reusv3i  5347  frpoinsg  6308  fimadmfo  6762  fimadmfoALT  6764  fvtresfn  6951  fvmpt3  6953  ffvelcdmd  7038  fnressn  7112  fsnex  7238  f1oiso2  7307  riota5f  7352  onsuc  7764  onsucuni  7779  frrlem10  8245  seqomlem2  8390  oaordi  8481  nnaordi  8554  qsdisj  8741  dom2lem  8939  canth2g  9069  limenpsi  9090  nnfi  9102  php4  9144  onfin  9149  sucxpdom  9171  dmfi  9245  fiin  9335  supiso  9389  ordiso2  9430  wdom2d  9495  elirrv  9512  infeq5  9558  cantnfp1lem3  9601  cantnflem1d  9609  rankwflemb  9717  onenon  9873  cardonle  9881  sdomsdomcardi  9895  acni  9967  cardaleph  10011  djuen  10092  djuinf  10111  infdju1  10112  nnadju  10120  pwsdompw  10125  infdif  10130  cfval  10169  fin34  10312  fin1a2lem1  10322  fin1a2  10337  ttukeylem6  10436  sdomsdomcard  10482  canth3  10483  fpwwe2  10566  canthwelem  10573  gchdju1  10579  pwfseqlem4  10585  gchdjuidm  10591  gchxpidm  10592  tskwe2  10696  rankcf  10700  tskuni  10706  gruxp  10730  dmrecnq  10891  lterpq  10893  archnq  10903  reclem3pr  10972  reclem4pr  10973  0idsr  11020  lep1  11996  ledivp1  12058  negfi  12105  supaddc  12123  supmul1  12125  suprzcl  12609  uz11  12813  zmin  12894  zbtwnre  12896  rpnnen1lem4  12930  rpnnen1lem5  12931  xnegid  13190  supxrre  13279  infxrre  13289  eluzfz2  13486  fzsuc  13525  fzsuc2  13536  fzp1disj  13537  fzneuz  13562  nn0p1elfzo  13657  fllep1  13760  fraclt1  13761  fracle1  13762  fracge0  13763  flhalf  13789  ceige  13803  ceim1l  13806  fldiv  13819  modval  13830  suppssfz  13956  seqeq1  13966  expubnd  14140  iexpcyc  14169  binom2sub1  14183  faclbnd4lem3  14257  pfxid  14647  pfxccatpfx2  14699  swrdccat3blem  14701  cshw0  14756  cshwn  14759  cshimadifsn  14791  cshimadifsn0  14792  pfx2  14909  trclexlem  14956  shftfval  15032  shftcan1  15045  reval  15068  cjmulrcl  15106  addcj  15110  absval  15200  absneg  15239  abscj  15241  sqabsadd  15244  sqabssub  15245  leabs  15261  sqreulem  15322  lo1res  15521  o1of2  15575  o1rlimmul  15581  fsumconst1  15753  flo1  15819  trirecip  15828  efcan  16061  efi4p  16104  resin4p  16105  recos4p  16106  sincossq  16143  ruclem10  16206  iddvds  16238  1dvds  16239  2ebits  16416  lcmftp  16605  coprmgcdb  16618  1idssfct  16649  exprmfct  16674  eulerthlem2  16752  odzphi  16767  pcprendvds  16811  pcmpt  16863  oddprmdvds  16874  vdwlem8  16959  0ram2  16992  prmgaplem7  17028  setsn0fun  17143  setsexstruct2  17145  pwsvscaval  17459  2initoinv  17977  initoeu1  17978  initoeu2lem1  17981  initoeu2  17983  2termoinv  17984  termoeu1  17985  homarel  18003  joinfval  18337  meetfval  18351  latjcom  18413  latmcom  18429  0subm  18785  sgrp2nmndlem5  18900  grprcan  18949  isgrpid2  18952  grpinvid  18975  mulgnn0z  19077  qus0  19164  eqg0subg  19171  ghmker  19217  symgbasmap  19352  symginv  19377  pmtrfrn  19433  odmulg2  19530  slwpgp  19588  pj1eq  19675  efgtf  19697  frgpinv  19739  frgpup2  19751  cnaddablx  19843  cnaddabl  19844  zaddablx  19847  imasabl  19851  dprdfadd  19997  dpjidcl  20035  dpjlid  20038  pgpfac1lem3  20054  omndmul2  20108  omndmul  20110  srgen1zr  20197  1unit  20354  unitgrpid  20365  1rinv  20375  irredn0  20403  irredneg  20410  c0snmgmhm  20442  rngisomring1  20448  zrrnghm  20513  rnrhmsubrg  20582  zrinitorngc  20619  zrtermorngc  20620  zrtermoringc  20652  isdrng2  20720  ringen1zr  20755  abv0  20800  abv1z  20801  abvneg  20803  orng0le1  20851  lmodfopne  20895  lsssn0  20943  lspsn0  21003  lsp0  21004  lmhmvsca  21040  lmhmrnlss  21045  lmhmkerlss  21046  lsppratlem5  21149  rsp1  21235  kerlidl  21276  ring2idlqus  21307  rngqiprngfulem4  21312  rngqiprngfu  21315  cnfldneg  21378  zringcyg  21449  chrid  21505  chrrhm  21511  ip0r  21617  ocvlss  21652  ocv1  21659  rlmassa  21850  psrbagfsupp  21899  snifpsrbag  21900  psrbaglefi  21906  psrvscaval  21929  psrdi  21943  psrdir  21944  mplvscaval  21994  mhpmpl  22110  mhpdeg  22111  mhppwdeg  22116  psdmul  22132  psdpw  22136  coe1sclmulfv  22248  coe1id  22258  ply1idvr1OLD  22260  evl1var  22301  mamuvs1  22370  mamuvs2  22371  matecl  22390  matvscacell  22401  mat0scmat  22503  submaval0  22545  mdetrsca  22568  maduval  22603  minmar1val0  22612  pmatcollpw3fi1lem2  22752  chcoeffeqlem  22850  cayleyhamilton0  22854  cayleyhamiltonALT  22856  toponsspwpw  22887  cctop  22971  cldval  22988  ntrfval  22989  clsfval  22990  cmclsopn  23027  opncldf3  23051  neifval  23064  lpfval  23103  cnrmnrm  23326  dis2ndc  23425  islocfin  23482  tx1cn  23574  idqtop  23671  kqtopon  23692  kqid  23693  kqcld  23700  hmphen2  23764  filssufil  23877  ufileu  23884  alexsublem  24009  efmndtmd  24066  symgtgp  24071  ustuqtop4  24209  cstucnd  24248  metustexhalf  24521  nm0  24594  rlmnlm  24653  nmolb  24682  metdseq0  24820  pi1xfrval  25021  clmvneg1  25066  clmvsubval  25076  ipcau2  25201  tcphcphlem1  25202  tcphcphlem2  25203  cmetcaulem  25255  ovolicc2lem3  25486  ovolicc2lem4  25487  mbfmulc2lem  25614  i1fpos  25673  mbfi1fseqlem3  25684  itg2ge0  25702  bddiblnc  25809  dvres2  25879  dvaddbr  25905  dvmulbr  25906  dvcobr  25913  dvfsumlem4  25996  ftc1a  26004  ftc1lem6  26008  uc1pmon1p  26117  ig1pval2  26142  dgradd2  26233  dgrcolem2  26239  plydivlem4  26262  plydiveu  26264  elqaalem3  26287  qaa  26289  ulmdvlem1  26365  abelthlem6  26401  abelthlem7  26403  eflogeq  26566  jensenlem2  26951  harmonicbnd4  26974  sgmnncl  27110  dchrptlem2  27228  1lgs  27303  lgs1  27304  2sqcoprm  27398  addsqnreup  27406  dchrisumlem2  27453  dchrisum0lem2a  27480  selberg2lem  27513  pntrsumo1  27528  pntrsumbnd  27529  pntpbnd1  27549  pntlemr  27565  pntlemj  27566  padicabvf  27594  bdayval  27612  noextendgt  27634  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetainflem4  27704  oldval  27826  divmuls  28213  divscl  28215  seqsp1  28303  bdayfinbndlem1  28459  zz12s  28467  remulscllem1  28492  incistruhgr  29148  subgrprop3  29345  subgruhgredgd  29353  usgrexi  29510  cusgrexi  29512  cusgrsizeinds  29521  vtxdgfusgrf  29566  1hevtxdg1  29575  1egrvtxdg1  29578  ewlkprop  29672  wlklenvm1  29690  wlkl1loop  29706  wlkp1lem4  29743  2pthnloop  29799  upgrclwlkcompim  29849  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem6  29883  crctcshwlkn0lem7  29884  crctcshlem4  29888  wspthnonp  29927  wlkswwlksf1o  29947  wwlksnwwlksnon  29983  umgr2wlkon  30018  wwlks2onv  30021  elwwlks2ons3im  30022  elwspths2spth  30038  umgrclwwlkge2  30061  clwlkclwwlkf1lem3  30076  erclwwlkref  30090  clwwlknp  30107  wwlksext2clwwlk  30127  wwlksubclwwlk  30128  0pthon1  30198  1wlkdlem4  30210  1pthd  30213  3spthd  30246  eupth2eucrct  30287  eucrctshift  30313  eucrct2eupth  30315  frgrncvvdeqlem8  30376  frgr2wwlkeqm  30401  isgrpoi  30569  grpoinvfval  30593  grpodivfval  30605  vcz  30646  cnaddabloOLD  30652  nvz0  30739  sspz  30806  lno0  30827  nmobndi  30846  ipasslem2  30903  shunssi  31439  ococin  31479  ssjo  31518  pjocini  31769  nlfnval  31952  lncnopbd  32108  riesz3i  32133  cnlnadjlem7  32144  pjclem4  32270  pj3si  32278  hstoc  32293  hstnmoc  32294  hstoh  32303  hst0  32304  mdsl2i  32393  chirredlem3  32463  chirredlem4  32464  dmdbr5ati  32493  rexunirn  32561  fcnvgreu  32745  infxrge0glb  32838  sgnneg  32906  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  isarchi3  33248  nsgqusf1olem2  33474  ssdifidllem  33516  ssmxidllem  33533  rprmdvdspow  33593  ressply1sub  33630  fedgmullem1  33773  extdg1id  33810  nn0constr  33905  zartopn  34019  zarcmplem  34025  esumcvg  34230  esumcvgre  34235  sigaval  34255  unelldsys  34302  fiunelros  34318  measval  34342  pmeasmono  34468  probfinmeasb  34572  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemsi  34659  ballotlemfrci  34672  signlem0  34731  breprexp  34777  bnj1006  35102  bnj1110  35124  bnj1253  35159  bnj1280  35162  bnj1463  35197  bnj1312  35200  fineqvinfep  35269  erdszelem7  35379  erdszelem8  35380  cvmliftlem10  35476  cvmliftlem13  35478  cvmlift2lem9  35493  cvmlift3lem6  35506  cvmlift3lem7  35507  cvmlift3lem9  35509  satfv1lem  35544  dfrdg2  35975  cldregopn  36513  tailfval  36554  filnetlem3  36562  filnetlem4  36563  ontopbas  36610  bj-nnfbd  37066  bj-elid4  37482  bj-imdiridlem  37499  f1omptsnlem  37652  icoreunrn  37675  relowlpssretop  37680  fvineqsnf1  37726  wl-sbal2  37889  unccur  37924  poimirlem1  37942  poimirlem2  37943  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem11  37952  poimirlem12  37953  poimirlem17  37958  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem28  37969  poimir  37974  ismblfin  37982  cnambfre  37989  ftc1cnnc  38013  dvasin  38025  ismtyres  38129  heiborlem8  38139  ghomidOLD  38210  rngosn6  38247  rngonegmn1l  38262  rngonegmn1r  38263  rngoneglmul  38264  rngonegrmul  38265  idlnegcl  38343  0idl  38346  0rngo  38348  smprngopr  38373  sucmapsuc  38810  cossex  38830  qsdisjALTV  39020  cnvepresdmqss  39058  mpets2  39276  lkrval  39534  ldualvaddval  39577  ldualvsval  39584  opoc1  39648  pmap0  40211  pmap1N  40213  pexmidALTN  40424  cdleme31fv  40836  cdlemg27b  41142  erngdvlem4  41437  erng0g  41440  erngdvlem4-rN  41445  dvalveclem  41471  dvh0g  41557  dih0cnv  41729  dih1rn  41733  dih1cnv  41734  doch0  41804  doch1  41805  lcfl7lem  41945  mapdheq  42174  hdmap1eq  42247  hdmapval2lem  42277  hgmapvvlem3  42371  zndvdchrrhm  42412  lcmineqlem13  42480  aks4d1p9  42527  primrootsunit1  42536  aks6d1c1p1  42546  aks6d1c1p6  42553  aks6d1c1p8  42554  sticksstones1  42585  sticksstones6  42590  sticksstones7  42591  sticksstones11  42595  sticksstones12a  42596  sticksstones12  42597  sticksstones22  42607  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  unitscyglem5  42638  renegid  42805  sn-0ne2  42838  remul01  42839  remulinvcom  42865  sn-0tie0  42896  renegmulnnass  42910  domnexpgn0cl  42968  abvexp  42977  frlmsnic  42985  fsuppssind  43026  mzpval  43164  mzpindd  43178  pellex  43263  2nn0ind  43373  jm2.26lem3  43429  pw2f1o2val  43467  wepwsolem  43470  fnwe2lem3  43480  lnmfg  43510  dgrsub2  43563  mpaaeu  43578  flcidc  43598  dflim5  43757  naddwordnexlem1  43825  rtrclexlem  44043  cnvrcl0  44052  brcoffn  44457  clsk1indlem3  44470  clsneif1o  44531  clsneicnv  44532  clsneikex  44533  clsneinex  44534  neicvgmex  44544  neicvgel1  44546  suprleubrd  44593  suprlubrd  44595  imo72b2  44599  dvconstbi  44761  bcc0  44767  binomcxplemnotnn0  44783  nnfoctb  45479  infleinflem1  45799  fprodcnlem  46029  sumnnodd  46060  icccncfext  46315  itgsin0pilem1  46378  stoweidlem32  46460  stoweidlem35  46463  stoweidlem36  46464  stoweidlem37  46465  stoweidlem43  46471  stoweidlem50  46478  wallispilem5  46497  stirlinglem2  46503  stirlinglem3  46504  stirlinglem4  46505  stirlinglem8  46509  stirlinglem11  46512  stirlinglem12  46513  stirlinglem14  46515  stirlinglem15  46516  fourierdlem11  46546  fourierdlem20  46555  fourierdlem21  46556  fourierdlem41  46576  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem64  46598  fourierdlem71  46605  fourierdlem79  46613  fourierdlem90  46624  fourierdlem91  46625  fourierswlem  46658  etransclem17  46679  etransclem38  46700  saluni  46753  meaiininclem  46914  issmflelem  47172  issmfgtlem  47183  issmfgelem  47197  smflimsuplem4  47251  f1cof1blem  47516  zplusmodne  47791  m1modne  47796  submodneaddmod  47799  nndivides2  47826  sprval  47933  prprval  47968  bgoldbtbndlem2  48276  bgoldbtbndlem3  48277  bgoldbtbnd  48279  isubgrvtxuhgr  48334  isubgredg  48336  grimcnv  48358  isuspgrim  48366  gricushgr  48387  uhgrimisgrgric  48401  grtriclwlk3  48415  isubgr3stgrlem7  48442  grlimgrtri  48473  grlictr  48485  gpgvtx0  48523  gpgvtx1  48524  gpgprismgrusgra  48528  gpgedgvtx1  48532  gpg3kgrtriex  48559  pgnbgreunbgrlem3  48588  pgnbgreunbgrlem6  48594  isclintop  48677  clintopcllaw  48681  nzrneg1ne0  48700  lidldomn1  48701  zlidlring  48704  uzlidlring  48705  2zrngnmlid  48725  cznrng  48731  blenre  49044  blennn  49045  2arymaptf  49122  itcoval1  49133  itcovalendof  49139  ehl2eudisval0  49195  eenglngeehlnmlem2  49208  itsclc0yqsol  49234  inlinecirc02plem  49256  ipolub  49457  ipoglb  49460  nelsubclem  49536  imaid  49623  imaf1co  49624  uptri  49683  uptrar  49685  uptrai  49686  oppc1stflem  49756  setrec2mpt  50166