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  3627  eueq2  3672  csbiegf  3886  difsnb  4760  reusv3i  5346  frpoinsg  6295  fimadmfo  6749  fimadmfoALT  6751  fvtresfn  6936  fvmpt3  6938  ffvelcdmd  7023  fnressn  7096  fsnex  7224  f1oiso2  7293  riota5f  7338  onsuc  7751  onsucuni  7767  frrlem10  8235  seqomlem2  8380  oaordi  8471  nnaordi  8543  qsdisj  8728  dom2lem  8924  canth2g  9055  limenpsi  9076  nnfi  9091  php4  9134  onfin  9139  sucxpdom  9160  xpfiOLD  9228  dmfi  9244  fiin  9331  supiso  9385  ordiso2  9426  wdom2d  9491  elirrv  9508  infeq5  9552  cantnfp1lem3  9595  cantnflem1d  9603  rankwflemb  9708  onenon  9864  cardonle  9872  sdomsdomcardi  9886  acni  9958  cardaleph  10002  djuen  10083  djuinf  10102  infdju1  10103  nnadju  10111  pwsdompw  10116  infdif  10121  cfval  10160  fin34  10303  fin1a2lem1  10313  fin1a2  10328  ttukeylem6  10427  sdomsdomcard  10473  canth3  10474  fpwwe2  10556  canthwelem  10563  gchdju1  10569  pwfseqlem4  10575  gchdjuidm  10581  gchxpidm  10582  tskwe2  10686  rankcf  10690  tskuni  10696  gruxp  10720  dmrecnq  10881  lterpq  10883  archnq  10893  reclem3pr  10962  reclem4pr  10963  0idsr  11010  lep1  11983  ledivp1  12045  negfi  12092  supaddc  12110  supmul1  12112  suprzcl  12574  uz11  12778  zmin  12863  zbtwnre  12865  rpnnen1lem4  12899  rpnnen1lem5  12900  xnegid  13158  supxrre  13247  infxrre  13257  eluzfz2  13453  fzsuc  13492  fzsuc2  13503  fzp1disj  13504  fzneuz  13529  nn0p1elfzo  13623  fllep1  13723  fraclt1  13724  fracle1  13725  fracge0  13726  flhalf  13752  ceige  13766  ceim1l  13769  fldiv  13782  modval  13793  suppssfz  13919  seqeq1  13929  expubnd  14103  iexpcyc  14132  binom2sub1  14146  faclbnd4lem3  14220  pfxid  14609  pfxccatpfx2  14661  swrdccat3blem  14663  cshw0  14718  cshwn  14721  cshimadifsn  14754  cshimadifsn0  14755  pfx2  14872  trclexlem  14919  shftfval  14995  shftcan1  15008  reval  15031  cjmulrcl  15069  addcj  15073  absval  15163  absneg  15202  abscj  15204  sqabsadd  15207  sqabssub  15208  leabs  15224  sqreulem  15285  lo1res  15484  o1of2  15538  o1rlimmul  15544  flo1  15779  trirecip  15788  efcan  16021  efi4p  16064  resin4p  16065  recos4p  16066  sincossq  16103  ruclem10  16166  iddvds  16198  1dvds  16199  2ebits  16376  lcmftp  16565  coprmgcdb  16578  1idssfct  16609  exprmfct  16633  eulerthlem2  16711  odzphi  16726  pcprendvds  16770  pcmpt  16822  oddprmdvds  16833  vdwlem8  16918  0ram2  16951  prmgaplem7  16987  setsn0fun  17102  setsexstruct2  17104  pwsvscaval  17417  2initoinv  17935  initoeu1  17936  initoeu2lem1  17939  initoeu2  17941  2termoinv  17942  termoeu1  17943  homarel  17961  joinfval  18295  meetfval  18309  latjcom  18371  latmcom  18387  0subm  18709  sgrp2nmndlem5  18821  grprcan  18870  isgrpid2  18873  grpinvid  18896  mulgnn0z  18998  0subgOLD  19049  qus0  19086  eqg0subg  19093  ghmker  19139  symgbasmap  19274  symginv  19299  pmtrfrn  19355  odmulg2  19452  slwpgp  19510  pj1eq  19597  efgtf  19619  frgpinv  19661  frgpup2  19673  cnaddablx  19765  cnaddabl  19766  zaddablx  19769  imasabl  19773  dprdfadd  19919  dpjidcl  19957  dpjlid  19960  pgpfac1lem3  19976  omndmul2  20030  omndmul  20032  srgen1zr  20119  1unit  20277  unitgrpid  20288  1rinv  20298  irredn0  20326  irredneg  20333  c0snmgmhm  20365  rngisomring1  20371  zrrnghm  20439  rnrhmsubrg  20508  zrinitorngc  20545  zrtermorngc  20546  zrtermoringc  20578  isdrng2  20646  ringen1zr  20681  abv0  20726  abv1z  20727  abvneg  20729  orng0le1  20777  lmodfopne  20821  lsssn0  20869  lspsn0  20929  lsp0  20930  lmhmvsca  20967  lmhmrnlss  20972  lmhmkerlss  20973  lsppratlem5  21076  rsp1  21162  kerlidl  21203  ring2idlqus  21234  rngqiprngfulem4  21239  rngqiprngfu  21242  cnfldneg  21320  zringcyg  21394  chrid  21450  chrrhm  21456  ip0r  21562  ocvlss  21597  ocv1  21604  rlmassa  21796  psrbagfsupp  21844  snifpsrbag  21845  psrbaglefi  21851  psrvscaval  21875  psrdi  21890  psrdir  21891  mplvscaval  21941  mhpmpl  22047  mhpdeg  22048  mhppwdeg  22053  psdmul  22069  psdpw  22073  coe1sclmulfv  22185  ply1idvr1OLD  22198  evl1var  22239  mamuvs1  22308  mamuvs2  22309  matecl  22328  matvscacell  22339  mat0scmat  22441  submaval0  22483  mdetrsca  22506  maduval  22541  minmar1val0  22550  pmatcollpw3fi1lem2  22690  chcoeffeqlem  22788  cayleyhamilton0  22792  cayleyhamiltonALT  22794  toponsspwpw  22825  cctop  22909  cldval  22926  ntrfval  22927  clsfval  22928  cmclsopn  22965  opncldf3  22989  neifval  23002  lpfval  23041  cnrmnrm  23264  dis2ndc  23363  islocfin  23420  tx1cn  23512  idqtop  23609  kqtopon  23630  kqid  23631  kqcld  23638  hmphen2  23702  filssufil  23815  ufileu  23822  alexsublem  23947  efmndtmd  24004  symgtgp  24009  ustuqtop4  24148  cstucnd  24187  metustexhalf  24460  nm0  24533  rlmnlm  24592  nmolb  24621  metdseq0  24759  pi1xfrval  24970  clmvneg1  25015  clmvsubval  25025  ipcau2  25150  tcphcphlem1  25151  tcphcphlem2  25152  cmetcaulem  25204  ovolicc2lem3  25436  ovolicc2lem4  25437  mbfmulc2lem  25564  i1fpos  25623  mbfi1fseqlem3  25634  itg2ge0  25652  bddiblnc  25759  dvres2  25829  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvcobr  25865  dvcobrOLD  25866  dvfsumlem4  25952  ftc1a  25960  ftc1lem6  25964  uc1pmon1p  26073  ig1pval2  26098  dgradd2  26190  dgrcolem2  26196  plydivlem4  26220  plydiveu  26222  elqaalem3  26245  qaa  26247  ulmdvlem1  26325  abelthlem6  26362  abelthlem7  26364  eflogeq  26527  jensenlem2  26914  harmonicbnd4  26937  sgmnncl  27073  dchrptlem2  27192  1lgs  27267  lgs1  27268  2sqcoprm  27362  addsqnreup  27370  dchrisumlem2  27417  dchrisum0lem2a  27444  selberg2lem  27477  pntrsumo1  27492  pntrsumbnd  27493  pntpbnd1  27513  pntlemr  27529  pntlemj  27530  padicabvf  27558  bdayval  27576  noextendgt  27598  nosupbnd2lem1  27643  noinfbnd2lem1  27658  noetainflem4  27668  oldval  27782  divsmul  28146  divscl  28148  seqsp1  28228  zzs12  28370  remulscllem1  28387  incistruhgr  29042  subgrprop3  29239  subgruhgredgd  29247  usgrexi  29404  cusgrexi  29406  cusgrsizeinds  29416  vtxdgfusgrf  29461  1hevtxdg1  29470  1egrvtxdg1  29473  ewlkprop  29567  wlklenvm1  29585  wlkl1loop  29601  wlkp1lem4  29638  2pthnloop  29694  upgrclwlkcompim  29744  crctcshwlkn0lem4  29776  crctcshwlkn0lem5  29777  crctcshwlkn0lem6  29778  crctcshwlkn0lem7  29779  crctcshlem4  29783  wspthnonp  29822  wlkswwlksf1o  29842  wwlksnwwlksnon  29878  umgr2wlkon  29913  wwlks2onv  29916  elwwlks2ons3im  29917  elwspths2spth  29930  umgrclwwlkge2  29953  clwlkclwwlkf1lem3  29968  erclwwlkref  29982  clwwlknp  29999  wwlksext2clwwlk  30019  wwlksubclwwlk  30020  0pthon1  30090  1wlkdlem4  30102  1pthd  30105  3spthd  30138  eupth2eucrct  30179  eucrctshift  30205  eucrct2eupth  30207  frgrncvvdeqlem8  30268  frgr2wwlkeqm  30293  isgrpoi  30460  grpoinvfval  30484  grpodivfval  30496  vcz  30537  cnaddabloOLD  30543  nvz0  30630  sspz  30697  lno0  30718  nmobndi  30737  ipasslem2  30794  shunssi  31330  ococin  31370  ssjo  31409  pjocini  31660  nlfnval  31843  lncnopbd  31999  riesz3i  32024  cnlnadjlem7  32035  pjclem4  32161  pj3si  32169  hstoc  32184  hstnmoc  32185  hstoh  32194  hst0  32195  mdsl2i  32284  chirredlem3  32354  chirredlem4  32355  dmdbr5ati  32384  rexunirn  32454  fcnvgreu  32630  infxrge0glb  32721  sgnneg  32791  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2lem7  33087  isarchi3  33139  nsgqusf1olem2  33361  ssdifidllem  33403  ssmxidllem  33420  rprmdvdspow  33480  ressply1sub  33515  fedgmullem1  33601  extdg1id  33637  nn0constr  33727  zartopn  33841  zarcmplem  33847  esumcvg  34052  esumcvgre  34057  sigaval  34077  unelldsys  34124  fiunelros  34140  measval  34164  pmeasmono  34291  probfinmeasb  34395  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemsi  34482  ballotlemfrci  34495  signlem0  34554  breprexp  34600  bnj1006  34926  bnj1110  34948  bnj1253  34983  bnj1280  34986  bnj1463  35021  bnj1312  35024  erdszelem7  35169  erdszelem8  35170  cvmliftlem10  35266  cvmliftlem13  35268  cvmlift2lem9  35283  cvmlift3lem6  35296  cvmlift3lem7  35297  cvmlift3lem9  35299  satfv1lem  35334  dfrdg2  35768  cldregopn  36304  tailfval  36345  filnetlem3  36353  filnetlem4  36354  ontopbas  36401  bj-elid4  37141  bj-imdiridlem  37158  f1omptsnlem  37309  icoreunrn  37332  relowlpssretop  37337  fvineqsnf1  37383  wl-sbal2  37537  unccur  37582  poimirlem1  37600  poimirlem2  37601  poimirlem4  37603  poimirlem6  37605  poimirlem7  37606  poimirlem11  37610  poimirlem12  37611  poimirlem17  37616  poimirlem20  37619  poimirlem22  37621  poimirlem23  37622  poimirlem28  37627  poimir  37632  ismblfin  37640  cnambfre  37647  ftc1cnnc  37671  dvasin  37683  ismtyres  37787  heiborlem8  37797  ghomidOLD  37868  rngosn6  37905  rngonegmn1l  37920  rngonegmn1r  37921  rngoneglmul  37922  rngonegrmul  37923  idlnegcl  38001  0idl  38004  0rngo  38006  smprngopr  38031  cossex  38395  qsdisjALTV  38591  cnvepresdmqss  38629  mpets2  38818  lkrval  39066  ldualvaddval  39109  ldualvsval  39116  opoc1  39180  pmap0  39744  pmap1N  39746  pexmidALTN  39957  cdleme31fv  40369  cdlemg27b  40675  erngdvlem4  40970  erng0g  40973  erngdvlem4-rN  40978  dvalveclem  41004  dvh0g  41090  dih0cnv  41262  dih1rn  41266  dih1cnv  41267  doch0  41337  doch1  41338  lcfl7lem  41478  mapdheq  41707  hdmap1eq  41780  hdmapval2lem  41810  hgmapvvlem3  41904  zndvdchrrhm  41945  lcmineqlem13  42014  aks4d1p9  42061  primrootsunit1  42070  aks6d1c1p1  42080  aks6d1c1p6  42087  aks6d1c1p8  42088  sticksstones1  42119  sticksstones6  42124  sticksstones7  42125  sticksstones11  42129  sticksstones12a  42130  sticksstones12  42131  sticksstones22  42141  aks6d1c6isolem1  42147  aks6d1c6isolem2  42148  unitscyglem5  42172  renegid  42346  sn-0ne2  42379  remul01  42380  remulinvcom  42406  sn-0tie0  42424  renegmulnnass  42438  domnexpgn0cl  42496  abvexp  42505  frlmsnic  42513  fsuppssind  42566  mzpval  42705  mzpindd  42719  pellex  42808  2nn0ind  42918  jm2.26lem3  42974  pw2f1o2val  43012  wepwsolem  43015  fnwe2lem3  43025  lnmfg  43055  dgrsub2  43108  mpaaeu  43123  flcidc  43143  dflim5  43302  naddwordnexlem1  43370  rtrclexlem  43589  cnvrcl0  43598  brcoffn  44003  clsk1indlem3  44016  clsneif1o  44077  clsneicnv  44078  clsneikex  44079  clsneinex  44080  neicvgmex  44090  neicvgel1  44092  suprleubrd  44139  suprlubrd  44141  imo72b2  44145  dvconstbi  44307  bcc0  44313  binomcxplemnotnn0  44329  nnfoctb  45026  infleinflem1  45350  fprodcnlem  45581  sumnnodd  45612  icccncfext  45869  itgsin0pilem1  45932  stoweidlem32  46014  stoweidlem35  46017  stoweidlem36  46018  stoweidlem37  46019  stoweidlem43  46025  stoweidlem50  46032  wallispilem5  46051  stirlinglem2  46057  stirlinglem3  46058  stirlinglem4  46059  stirlinglem8  46063  stirlinglem11  46066  stirlinglem12  46067  stirlinglem14  46069  stirlinglem15  46070  fourierdlem11  46100  fourierdlem20  46109  fourierdlem21  46110  fourierdlem41  46130  fourierdlem42  46131  fourierdlem48  46136  fourierdlem49  46137  fourierdlem64  46152  fourierdlem71  46159  fourierdlem79  46167  fourierdlem90  46178  fourierdlem91  46179  fourierswlem  46212  etransclem17  46233  etransclem38  46254  saluni  46307  meaiininclem  46468  issmflelem  46726  issmfgtlem  46737  issmfgelem  46751  smflimsuplem4  46805  f1cof1blem  47059  zplusmodne  47328  m1modne  47333  submodneaddmod  47336  sprval  47464  prprval  47499  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  bgoldbtbnd  47794  isubgrvtxuhgr  47848  isubgredg  47850  grimcnv  47872  isuspgrim  47880  gricushgr  47901  uhgrimisgrgric  47915  grtriclwlk3  47928  isubgr3stgrlem7  47955  grlimgrtri  47979  grlictr  47991  gpgvtx0  48028  gpgvtx1  48029  gpgprismgrusgra  48033  gpgedgvtx1  48037  gpg3kgrtriex  48064  pgnbgreunbgrlem3  48092  pgnbgreunbgrlem6  48098  isclintop  48179  clintopcllaw  48183  nzrneg1ne0  48202  lidldomn1  48203  zlidlring  48206  uzlidlring  48207  2zrngnmlid  48227  cznrng  48233  coe1id  48357  blenre  48547  blennn  48548  2arymaptf  48625  itcoval1  48636  itcovalendof  48642  ehl2eudisval0  48698  eenglngeehlnmlem2  48711  itsclc0yqsol  48737  inlinecirc02plem  48759  ipolub  48960  ipoglb  48963  nelsubclem  49040  imaid  49127  imaf1co  49128  uptri  49187  uptrar  49189  uptrai  49190  oppc1stflem  49260  setrec2mpt  49670