Theorem mpdan 685

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 582	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  mpidan  687  mpan2  689  biadanid  821  mpjaodan  956  mpjao3dan  1428  mpd3an3  1458  elabd2  3656  eueq2  3703  csbiegf  3924  difsnb  4810  reusv3i  5403  frpoinsg  6349  fimadmfo  6817  fimadmfoALT  6819  fvtresfn  7004  fvmpt3  7006  ffvelcdmd  7092  fnressn  7165  fsnex  7290  f1oiso2  7357  riota5f  7402  onsuc  7813  onsucuni  7830  frrlem10  8299  seqomlem2  8470  oaordi  8565  nnaordi  8637  qsdisj  8811  dom2lem  9011  canth2g  9154  limenpsi  9175  nnfi  9190  php4  9236  onfin  9253  sucxpdom  9278  xpfiOLD  9342  dmfi  9354  pwfilemOLD  9370  pwfiOLD  9371  fiin  9445  supiso  9498  ordiso2  9538  wdom2d  9603  infeq5  9660  cantnfp1lem3  9703  cantnflem1d  9711  rankwflemb  9816  onenon  9972  cardonle  9980  sdomsdomcardi  9994  acni  10068  cardaleph  10112  djuen  10192  djuinf  10211  infdju1  10212  nnadju  10220  pwsdompw  10227  infdif  10232  cfval  10270  fin34  10413  fin1a2lem1  10423  fin1a2  10438  ttukeylem6  10537  sdomsdomcard  10583  canth3  10584  fpwwe2  10666  canthwelem  10673  gchdju1  10679  pwfseqlem4  10685  gchdjuidm  10691  gchxpidm  10692  tskwe2  10796  rankcf  10800  tskuni  10806  gruxp  10830  dmrecnq  10991  lterpq  10993  archnq  11003  reclem3pr  11072  reclem4pr  11073  0idsr  11120  lep1  12085  ledivp1  12146  negfi  12193  supaddc  12211  supmul1  12213  suprzcl  12672  uz11  12877  zmin  12958  zbtwnre  12960  rpnnen1lem4  12994  rpnnen1lem5  12995  xnegid  13249  supxrre  13338  infxrre  13347  eluzfz2  13541  fzsuc  13580  fzsuc2  13591  fzp1disj  13592  fzneuz  13614  nn0p1elfzo  13707  fllep1  13798  fraclt1  13799  fracle1  13800  fracge0  13801  flhalf  13827  ceige  13841  ceim1l  13844  fldiv  13857  modval  13868  suppssfz  13991  seqeq1  14001  expubnd  14173  iexpcyc  14202  binom2sub1  14215  faclbnd4lem3  14286  pfxid  14666  pfxccatpfx2  14719  swrdccat3blem  14721  cshw0  14776  cshwn  14779  cshimadifsn  14812  cshimadifsn0  14813  pfx2  14930  trclexlem  14973  shftfval  15049  shftcan1  15062  reval  15085  cjmulrcl  15123  addcj  15127  absval  15217  absneg  15256  abscj  15258  sqabsadd  15261  sqabssub  15262  leabs  15278  sqreulem  15338  lo1res  15535  o1of2  15589  o1rlimmul  15595  flo1  15832  trirecip  15841  efcan  16072  efi4p  16113  resin4p  16114  recos4p  16115  sincossq  16152  ruclem10  16215  iddvds  16246  1dvds  16247  2ebits  16421  lcmftp  16606  coprmgcdb  16619  1idssfct  16650  exprmfct  16674  eulerthlem2  16750  odzphi  16764  pcprendvds  16808  pcmpt  16860  oddprmdvds  16871  vdwlem8  16956  0ram2  16989  prmgaplem7  17025  setsn0fun  17141  setsexstruct2  17143  pwsvscaval  17476  2initoinv  17998  initoeu1  17999  initoeu2lem1  18002  initoeu2  18004  2termoinv  18005  termoeu1  18006  homarel  18024  joinfval  18364  meetfval  18378  latjcom  18438  latmcom  18454  0subm  18773  sgrp2nmndlem5  18885  grprcan  18934  isgrpid2  18937  grpinvid  18960  mulgnn0z  19060  0subgOLD  19111  qus0  19148  eqg0subg  19155  ghmker  19200  symgbasmap  19335  symginv  19361  pmtrfrn  19417  odmulg2  19514  slwpgp  19572  pj1eq  19659  efgtf  19681  frgpinv  19723  frgpup2  19735  cnaddablx  19827  cnaddabl  19828  zaddablx  19831  imasabl  19835  dprdfadd  19981  dpjidcl  20019  dpjlid  20022  pgpfac1lem3  20038  srgen1zr  20160  1unit  20317  unitgrpid  20328  1rinv  20338  irredn0  20366  irredneg  20373  c0snmgmhm  20405  rngisomring1  20411  zrrnghm  20477  rnrhmsubrg  20548  zrinitorngc  20579  zrtermorngc  20580  zrtermoringc  20612  isdrng2  20642  ringen1zr  20670  abv0  20715  abv1z  20716  abvneg  20718  lmodfopne  20787  lsssn0  20836  lspsn0  20896  lsp0  20897  lmhmvsca  20934  lmhmrnlss  20939  lmhmkerlss  20940  lsppratlem5  21043  rsp1  21137  ring2idlqus  21203  rngqiprngfulem4  21208  rngqiprngfu  21211  cnfldneg  21327  zringcyg  21399  chrid  21459  chrrhm  21465  ip0r  21573  ocvlss  21608  ocv1  21615  rlmassa  21808  psrbagfsupp  21857  snifpsrbag  21859  psrbaglefi  21869  psrvscaval  21899  psrdi  21914  psrdir  21915  mplvscaval  21965  mhpmpl  22076  mhpdeg  22077  mhppwdeg  22082  psdmul  22098  coe1sclmulfv  22211  ply1idvr1  22223  evl1var  22264  mamuvs1  22335  mamuvs2  22336  matecl  22357  matvscacell  22368  mat0scmat  22470  submaval0  22512  mdetrsca  22535  maduval  22570  minmar1val0  22579  pmatcollpw3fi1lem2  22719  chcoeffeqlem  22817  cayleyhamilton0  22821  cayleyhamiltonALT  22823  toponsspwpw  22854  cctop  22939  cldval  22957  ntrfval  22958  clsfval  22959  cmclsopn  22996  opncldf3  23020  neifval  23033  lpfval  23072  cnrmnrm  23295  dis2ndc  23394  islocfin  23451  tx1cn  23543  idqtop  23640  kqtopon  23661  kqid  23662  kqcld  23669  hmphen2  23733  filssufil  23846  ufileu  23853  alexsublem  23978  efmndtmd  24035  symgtgp  24040  ustuqtop4  24179  cstucnd  24219  metustexhalf  24495  nm0  24568  rlmnlm  24635  nmolb  24664  metdseq0  24800  pi1xfrval  25011  clmvneg1  25056  clmvsubval  25066  ipcau2  25192  tcphcphlem1  25193  tcphcphlem2  25194  cmetcaulem  25246  ovolicc2lem3  25478  ovolicc2lem4  25479  mbfmulc2lem  25606  i1fpos  25666  mbfi1fseqlem3  25677  itg2ge0  25695  bddiblnc  25801  dvres2  25871  dvaddbr  25898  dvmulbr  25899  dvmulbrOLD  25900  dvcobr  25907  dvcobrOLD  25908  dvfsumlem4  25994  ftc1a  26002  ftc1lem6  26006  uc1pmon1p  26117  ig1pval2  26141  dgradd2  26233  dgrcolem2  26239  plydivlem4  26261  plydiveu  26263  elqaalem3  26286  qaa  26288  ulmdvlem1  26366  abelthlem6  26403  abelthlem7  26405  eflogeq  26566  jensenlem2  26950  harmonicbnd4  26973  sgmnncl  27109  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  27611  noextendgt  27633  nosupbnd2lem1  27678  noinfbnd2lem1  27693  noetainflem4  27703  oldval  27811  divsmul  28153  divscl  28155  seqsp1  28218  remulscllem1  28284  incistruhgr  28948  subgrprop3  29145  subgruhgredgd  29153  usgrexi  29310  cusgrexi  29312  cusgrsizeinds  29322  vtxdgfusgrf  29367  1hevtxdg1  29376  1egrvtxdg1  29379  ewlkprop  29473  wlklenvm1  29492  wlkl1loop  29508  wlkp1lem4  29546  2pthnloop  29601  upgrclwlkcompim  29651  crctcshwlkn0lem4  29680  crctcshwlkn0lem5  29681  crctcshwlkn0lem6  29682  crctcshwlkn0lem7  29683  crctcshlem4  29687  wspthnonp  29726  wlkswwlksf1o  29746  wwlksnwwlksnon  29782  umgr2wlkon  29817  wwlks2onv  29820  elwwlks2ons3im  29821  elwspths2spth  29834  umgrclwwlkge2  29857  clwlkclwwlkf1lem3  29872  erclwwlkref  29886  clwwlknp  29903  wwlksext2clwwlk  29923  wwlksubclwwlk  29924  0pthon1  29994  1wlkdlem4  30006  1pthd  30009  3spthd  30042  eupth2eucrct  30083  eucrctshift  30109  eucrct2eupth  30111  frgrncvvdeqlem8  30172  frgr2wwlkeqm  30197  isgrpoi  30364  grpoinvfval  30388  grpodivfval  30400  vcz  30441  cnaddabloOLD  30447  nvz0  30534  sspz  30601  lno0  30622  nmobndi  30641  ipasslem2  30698  shunssi  31234  ococin  31274  ssjo  31313  pjocini  31564  nlfnval  31747  lncnopbd  31903  riesz3i  31928  cnlnadjlem7  31939  pjclem4  32065  pj3si  32073  hstoc  32088  hstnmoc  32089  hstoh  32098  hst0  32099  mdsl2i  32188  chirredlem3  32258  chirredlem4  32259  dmdbr5ati  32288  rexunirn  32347  fcnvgreu  32516  infxrge0glb  32592  omndmul2  32849  omndmul  32851  cycpmco2lem5  32908  cycpmco2lem6  32909  cycpmco2lem7  32910  isarchi3  32952  orng0le1  33087  nsgqusf1olem2  33186  kerlidl  33196  ssmxidllem  33248  rprmdvdspow  33303  ressply1sub  33325  fedgmullem1  33397  extdg1id  33425  zartopn  33546  zarcmplem  33552  esumcvg  33775  esumcvgre  33780  sigaval  33800  unelldsys  33847  fiunelros  33863  measval  33887  pmeasmono  34014  probfinmeasb  34118  ballotlemfc0  34182  ballotlemfcc  34183  ballotlemsi  34204  ballotlemfrci  34217  sgnneg  34230  signlem0  34289  breprexp  34335  bnj1006  34661  bnj1110  34683  bnj1253  34718  bnj1280  34721  bnj1463  34756  bnj1312  34759  erdszelem7  34877  erdszelem8  34878  cvmliftlem10  34974  cvmliftlem13  34976  cvmlift2lem9  34991  cvmlift3lem6  35004  cvmlift3lem7  35005  cvmlift3lem9  35007  satfv1lem  35042  dfrdg2  35461  cldregopn  35885  tailfval  35926  filnetlem3  35934  filnetlem4  35935  ontopbas  35982  bj-elid4  36717  bj-imdiridlem  36734  f1omptsnlem  36885  icoreunrn  36908  relowlpssretop  36913  fvineqsnf1  36959  wl-sbal2  37101  unccur  37146  poimirlem1  37164  poimirlem2  37165  poimirlem4  37167  poimirlem6  37169  poimirlem7  37170  poimirlem11  37174  poimirlem12  37175  poimirlem17  37180  poimirlem20  37183  poimirlem22  37185  poimirlem23  37186  poimirlem28  37191  poimir  37196  ismblfin  37204  cnambfre  37211  ftc1cnnc  37235  dvasin  37247  ismtyres  37351  heiborlem8  37361  ghomidOLD  37432  rngosn6  37469  rngonegmn1l  37484  rngonegmn1r  37485  rngoneglmul  37486  rngonegrmul  37487  idlnegcl  37565  0idl  37568  0rngo  37570  smprngopr  37595  cossex  37960  qsdisjALTV  38156  cnvepresdmqss  38193  mpets2  38382  lkrval  38629  ldualvaddval  38672  ldualvsval  38679  opoc1  38743  pmap0  39307  pmap1N  39309  pexmidALTN  39520  cdleme31fv  39932  cdlemg27b  40238  erngdvlem4  40533  erng0g  40536  erngdvlem4-rN  40541  dvalveclem  40567  dvh0g  40653  dih0cnv  40825  dih1rn  40829  dih1cnv  40830  doch0  40900  doch1  40901  lcfl7lem  41041  mapdheq  41270  hdmap1eq  41343  hdmapval2lem  41373  hgmapvvlem3  41467  lcmineqlem13  41581  aks4d1p9  41628  primrootsunit1  41636  aks6d1c1p1  41647  aks6d1c1p6  41654  aks6d1c1p8  41655  sticksstones1  41687  sticksstones6  41692  sticksstones7  41693  sticksstones11  41697  sticksstones12a  41698  sticksstones12  41699  sticksstones22  41709  aks6d1c6isolem1  41715  aks6d1c6isolem2  41716  frlmsnic  41838  fsuppssind  41891  renegid  41993  sn-0ne2  42026  remul01  42027  remulinvcom  42052  sn-0tie0  42059  renegmulnnass  42073  sn-inelr  42085  mzpval  42217  mzpindd  42231  pellex  42320  2nn0ind  42431  jm2.26lem3  42487  pw2f1o2val  42525  wepwsolem  42531  fnwe2lem3  42541  lnmfg  42571  dgrsub2  42624  mpaaeu  42639  flcidc  42663  dflim5  42823  naddwordnexlem1  42892  rtrclexlem  43111  cnvrcl0  43120  brcoffn  43525  clsk1indlem3  43538  clsneif1o  43599  clsneicnv  43600  clsneikex  43601  clsneinex  43602  neicvgmex  43612  neicvgel1  43614  suprleubrd  43661  suprlubrd  43663  imo72b2  43667  dvconstbi  43836  bcc0  43842  binomcxplemnotnn0  43858  nnfoctb  44476  infleinflem1  44815  fprodcnlem  45050  sumnnodd  45081  icccncfext  45338  itgsin0pilem1  45401  stoweidlem32  45483  stoweidlem35  45486  stoweidlem36  45487  stoweidlem37  45488  stoweidlem43  45494  stoweidlem50  45501  wallispilem5  45520  stirlinglem2  45526  stirlinglem3  45527  stirlinglem4  45528  stirlinglem8  45532  stirlinglem11  45535  stirlinglem12  45536  stirlinglem14  45538  stirlinglem15  45539  fourierdlem11  45569  fourierdlem20  45578  fourierdlem21  45579  fourierdlem41  45599  fourierdlem42  45600  fourierdlem48  45605  fourierdlem49  45606  fourierdlem64  45621  fourierdlem71  45628  fourierdlem79  45636  fourierdlem90  45647  fourierdlem91  45648  fourierswlem  45681  etransclem17  45702  etransclem38  45723  saluni  45776  meaiininclem  45937  issmflelem  46195  issmfgtlem  46206  issmfgelem  46220  smflimsuplem4  46274  f1cof1blem  46519  sprval  46882  prprval  46917  bgoldbtbndlem2  47209  bgoldbtbndlem3  47210  bgoldbtbnd  47212  isubgrvtxuhgr  47262  isuspgrim  47285  grimcnv  47289  gricushgr  47295  isclintop  47381  clintopcllaw  47385  nzrneg1ne0  47404  lidldomn1  47405  zlidlring  47408  uzlidlring  47409  2zrngnmlid  47429  cznrng  47435  coe1id  47564  blenre  47759  blennn  47760  2arymaptf  47837  itcoval1  47848  itcovalendof  47854  ehl2eudisval0  47910  eenglngeehlnmlem2  47923  itsclc0yqsol  47949  inlinecirc02plem  47971  ipolub  48111  ipoglb  48114  setrec2mpt  48240