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  3620  eueq2  3664  csbiegf  3878  difsnb  4757  reusv3i  5344  frpoinsg  6296  fimadmfo  6750  fimadmfoALT  6752  fvtresfn  6937  fvmpt3  6939  ffvelcdmd  7024  fnressn  7097  fsnex  7223  f1oiso2  7292  riota5f  7337  onsuc  7749  onsucuni  7764  frrlem10  8231  seqomlem2  8376  oaordi  8467  nnaordi  8539  qsdisj  8724  dom2lem  8920  canth2g  9050  limenpsi  9071  nnfi  9083  php4  9125  onfin  9130  sucxpdom  9151  dmfi  9225  fiin  9312  supiso  9366  ordiso2  9407  wdom2d  9472  elirrv  9489  infeq5  9533  cantnfp1lem3  9576  cantnflem1d  9584  rankwflemb  9692  onenon  9848  cardonle  9856  sdomsdomcardi  9870  acni  9942  cardaleph  9986  djuen  10067  djuinf  10086  infdju1  10087  nnadju  10095  pwsdompw  10100  infdif  10105  cfval  10144  fin34  10287  fin1a2lem1  10297  fin1a2  10312  ttukeylem6  10411  sdomsdomcard  10457  canth3  10458  fpwwe2  10540  canthwelem  10547  gchdju1  10553  pwfseqlem4  10559  gchdjuidm  10565  gchxpidm  10566  tskwe2  10670  rankcf  10674  tskuni  10680  gruxp  10704  dmrecnq  10865  lterpq  10867  archnq  10877  reclem3pr  10946  reclem4pr  10947  0idsr  10994  lep1  11968  ledivp1  12030  negfi  12077  supaddc  12095  supmul1  12097  suprzcl  12559  uz11  12763  zmin  12848  zbtwnre  12850  rpnnen1lem4  12884  rpnnen1lem5  12885  xnegid  13143  supxrre  13232  infxrre  13242  eluzfz2  13438  fzsuc  13477  fzsuc2  13488  fzp1disj  13489  fzneuz  13514  nn0p1elfzo  13608  fllep1  13711  fraclt1  13712  fracle1  13713  fracge0  13714  flhalf  13740  ceige  13754  ceim1l  13757  fldiv  13770  modval  13781  suppssfz  13907  seqeq1  13917  expubnd  14091  iexpcyc  14120  binom2sub1  14134  faclbnd4lem3  14208  pfxid  14598  pfxccatpfx2  14650  swrdccat3blem  14652  cshw0  14707  cshwn  14710  cshimadifsn  14742  cshimadifsn0  14743  pfx2  14860  trclexlem  14907  shftfval  14983  shftcan1  14996  reval  15019  cjmulrcl  15057  addcj  15061  absval  15151  absneg  15190  abscj  15192  sqabsadd  15195  sqabssub  15196  leabs  15212  sqreulem  15273  lo1res  15472  o1of2  15526  o1rlimmul  15532  flo1  15767  trirecip  15776  efcan  16009  efi4p  16052  resin4p  16053  recos4p  16054  sincossq  16091  ruclem10  16154  iddvds  16186  1dvds  16187  2ebits  16364  lcmftp  16553  coprmgcdb  16566  1idssfct  16597  exprmfct  16621  eulerthlem2  16699  odzphi  16714  pcprendvds  16758  pcmpt  16810  oddprmdvds  16821  vdwlem8  16906  0ram2  16939  prmgaplem7  16975  setsn0fun  17090  setsexstruct2  17092  pwsvscaval  17405  2initoinv  17923  initoeu1  17924  initoeu2lem1  17927  initoeu2  17929  2termoinv  17930  termoeu1  17931  homarel  17949  joinfval  18283  meetfval  18297  latjcom  18359  latmcom  18375  0subm  18731  sgrp2nmndlem5  18843  grprcan  18892  isgrpid2  18895  grpinvid  18918  mulgnn0z  19020  qus0  19107  eqg0subg  19114  ghmker  19160  symgbasmap  19295  symginv  19320  pmtrfrn  19376  odmulg2  19473  slwpgp  19531  pj1eq  19618  efgtf  19640  frgpinv  19682  frgpup2  19694  cnaddablx  19786  cnaddabl  19787  zaddablx  19790  imasabl  19794  dprdfadd  19940  dpjidcl  19978  dpjlid  19981  pgpfac1lem3  19997  omndmul2  20051  omndmul  20053  srgen1zr  20140  1unit  20298  unitgrpid  20309  1rinv  20319  irredn0  20347  irredneg  20354  c0snmgmhm  20386  rngisomring1  20392  zrrnghm  20457  rnrhmsubrg  20526  zrinitorngc  20563  zrtermorngc  20564  zrtermoringc  20596  isdrng2  20664  ringen1zr  20699  abv0  20744  abv1z  20745  abvneg  20747  orng0le1  20795  lmodfopne  20839  lsssn0  20887  lspsn0  20947  lsp0  20948  lmhmvsca  20985  lmhmrnlss  20990  lmhmkerlss  20991  lsppratlem5  21094  rsp1  21180  kerlidl  21221  ring2idlqus  21252  rngqiprngfulem4  21257  rngqiprngfu  21260  cnfldneg  21338  zringcyg  21412  chrid  21468  chrrhm  21474  ip0r  21580  ocvlss  21615  ocv1  21622  rlmassa  21814  psrbagfsupp  21862  snifpsrbag  21863  psrbaglefi  21869  psrvscaval  21893  psrdi  21908  psrdir  21909  mplvscaval  21959  mhpmpl  22065  mhpdeg  22066  mhppwdeg  22071  psdmul  22087  psdpw  22091  coe1sclmulfv  22203  ply1idvr1OLD  22216  evl1var  22257  mamuvs1  22326  mamuvs2  22327  matecl  22346  matvscacell  22357  mat0scmat  22459  submaval0  22501  mdetrsca  22524  maduval  22559  minmar1val0  22568  pmatcollpw3fi1lem2  22708  chcoeffeqlem  22806  cayleyhamilton0  22810  cayleyhamiltonALT  22812  toponsspwpw  22843  cctop  22927  cldval  22944  ntrfval  22945  clsfval  22946  cmclsopn  22983  opncldf3  23007  neifval  23020  lpfval  23059  cnrmnrm  23282  dis2ndc  23381  islocfin  23438  tx1cn  23530  idqtop  23627  kqtopon  23648  kqid  23649  kqcld  23656  hmphen2  23720  filssufil  23833  ufileu  23840  alexsublem  23965  efmndtmd  24022  symgtgp  24027  ustuqtop4  24165  cstucnd  24204  metustexhalf  24477  nm0  24550  rlmnlm  24609  nmolb  24638  metdseq0  24776  pi1xfrval  24987  clmvneg1  25032  clmvsubval  25042  ipcau2  25167  tcphcphlem1  25168  tcphcphlem2  25169  cmetcaulem  25221  ovolicc2lem3  25453  ovolicc2lem4  25454  mbfmulc2lem  25581  i1fpos  25640  mbfi1fseqlem3  25651  itg2ge0  25669  bddiblnc  25776  dvres2  25846  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvcobr  25882  dvcobrOLD  25883  dvfsumlem4  25969  ftc1a  25977  ftc1lem6  25981  uc1pmon1p  26090  ig1pval2  26115  dgradd2  26207  dgrcolem2  26213  plydivlem4  26237  plydiveu  26239  elqaalem3  26262  qaa  26264  ulmdvlem1  26342  abelthlem6  26379  abelthlem7  26381  eflogeq  26544  jensenlem2  26931  harmonicbnd4  26954  sgmnncl  27090  dchrptlem2  27209  1lgs  27284  lgs1  27285  2sqcoprm  27379  addsqnreup  27387  dchrisumlem2  27434  dchrisum0lem2a  27461  selberg2lem  27494  pntrsumo1  27509  pntrsumbnd  27510  pntpbnd1  27530  pntlemr  27546  pntlemj  27547  padicabvf  27575  bdayval  27593  noextendgt  27615  nosupbnd2lem1  27660  noinfbnd2lem1  27675  noetainflem4  27685  oldval  27801  divsmul  28165  divscl  28167  seqsp1  28247  zzs12  28391  remulscllem1  28408  incistruhgr  29064  subgrprop3  29261  subgruhgredgd  29269  usgrexi  29426  cusgrexi  29428  cusgrsizeinds  29438  vtxdgfusgrf  29483  1hevtxdg1  29492  1egrvtxdg1  29495  ewlkprop  29589  wlklenvm1  29607  wlkl1loop  29623  wlkp1lem4  29660  2pthnloop  29716  upgrclwlkcompim  29766  crctcshwlkn0lem4  29798  crctcshwlkn0lem5  29799  crctcshwlkn0lem6  29800  crctcshwlkn0lem7  29801  crctcshlem4  29805  wspthnonp  29844  wlkswwlksf1o  29864  wwlksnwwlksnon  29900  umgr2wlkon  29935  wwlks2onv  29938  elwwlks2ons3im  29939  elwspths2spth  29955  umgrclwwlkge2  29978  clwlkclwwlkf1lem3  29993  erclwwlkref  30007  clwwlknp  30024  wwlksext2clwwlk  30044  wwlksubclwwlk  30045  0pthon1  30115  1wlkdlem4  30127  1pthd  30130  3spthd  30163  eupth2eucrct  30204  eucrctshift  30230  eucrct2eupth  30232  frgrncvvdeqlem8  30293  frgr2wwlkeqm  30318  isgrpoi  30485  grpoinvfval  30509  grpodivfval  30521  vcz  30562  cnaddabloOLD  30568  nvz0  30655  sspz  30722  lno0  30743  nmobndi  30762  ipasslem2  30819  shunssi  31355  ococin  31395  ssjo  31434  pjocini  31685  nlfnval  31868  lncnopbd  32024  riesz3i  32049  cnlnadjlem7  32060  pjclem4  32186  pj3si  32194  hstoc  32209  hstnmoc  32210  hstoh  32219  hst0  32220  mdsl2i  32309  chirredlem3  32379  chirredlem4  32380  dmdbr5ati  32409  rexunirn  32478  fcnvgreu  32662  infxrge0glb  32755  sgnneg  32823  cycpmco2lem5  33106  cycpmco2lem6  33107  cycpmco2lem7  33108  isarchi3  33163  nsgqusf1olem2  33386  ssdifidllem  33428  ssmxidllem  33445  rprmdvdspow  33505  ressply1sub  33540  fedgmullem1  33649  extdg1id  33686  nn0constr  33781  zartopn  33895  zarcmplem  33901  esumcvg  34106  esumcvgre  34111  sigaval  34131  unelldsys  34178  fiunelros  34194  measval  34218  pmeasmono  34344  probfinmeasb  34448  ballotlemfc0  34513  ballotlemfcc  34514  ballotlemsi  34535  ballotlemfrci  34548  signlem0  34607  breprexp  34653  bnj1006  34979  bnj1110  35001  bnj1253  35036  bnj1280  35039  bnj1463  35074  bnj1312  35077  erdszelem7  35248  erdszelem8  35249  cvmliftlem10  35345  cvmliftlem13  35347  cvmlift2lem9  35362  cvmlift3lem6  35375  cvmlift3lem7  35376  cvmlift3lem9  35378  satfv1lem  35413  dfrdg2  35844  cldregopn  36382  tailfval  36423  filnetlem3  36431  filnetlem4  36432  ontopbas  36479  bj-elid4  37219  bj-imdiridlem  37236  f1omptsnlem  37387  icoreunrn  37410  relowlpssretop  37415  fvineqsnf1  37461  wl-sbal2  37615  unccur  37649  poimirlem1  37667  poimirlem2  37668  poimirlem4  37670  poimirlem6  37672  poimirlem7  37673  poimirlem11  37677  poimirlem12  37678  poimirlem17  37683  poimirlem20  37686  poimirlem22  37688  poimirlem23  37689  poimirlem28  37694  poimir  37699  ismblfin  37707  cnambfre  37714  ftc1cnnc  37738  dvasin  37750  ismtyres  37854  heiborlem8  37864  ghomidOLD  37935  rngosn6  37972  rngonegmn1l  37987  rngonegmn1r  37988  rngoneglmul  37989  rngonegrmul  37990  idlnegcl  38068  0idl  38071  0rngo  38073  smprngopr  38098  sucmapsuc  38507  cossex  38527  qsdisjALTV  38717  cnvepresdmqss  38756  mpets2  38945  lkrval  39193  ldualvaddval  39236  ldualvsval  39243  opoc1  39307  pmap0  39870  pmap1N  39872  pexmidALTN  40083  cdleme31fv  40495  cdlemg27b  40801  erngdvlem4  41096  erng0g  41099  erngdvlem4-rN  41104  dvalveclem  41130  dvh0g  41216  dih0cnv  41388  dih1rn  41392  dih1cnv  41393  doch0  41463  doch1  41464  lcfl7lem  41604  mapdheq  41833  hdmap1eq  41906  hdmapval2lem  41936  hgmapvvlem3  42030  zndvdchrrhm  42071  lcmineqlem13  42140  aks4d1p9  42187  primrootsunit1  42196  aks6d1c1p1  42206  aks6d1c1p6  42213  aks6d1c1p8  42214  sticksstones1  42245  sticksstones6  42250  sticksstones7  42251  sticksstones11  42255  sticksstones12a  42256  sticksstones12  42257  sticksstones22  42267  aks6d1c6isolem1  42273  aks6d1c6isolem2  42274  unitscyglem5  42298  renegid  42472  sn-0ne2  42505  remul01  42506  remulinvcom  42532  sn-0tie0  42550  renegmulnnass  42564  domnexpgn0cl  42622  abvexp  42631  frlmsnic  42639  fsuppssind  42692  mzpval  42830  mzpindd  42844  pellex  42933  2nn0ind  43043  jm2.26lem3  43099  pw2f1o2val  43137  wepwsolem  43140  fnwe2lem3  43150  lnmfg  43180  dgrsub2  43233  mpaaeu  43248  flcidc  43268  dflim5  43427  naddwordnexlem1  43495  rtrclexlem  43714  cnvrcl0  43723  brcoffn  44128  clsk1indlem3  44141  clsneif1o  44202  clsneicnv  44203  clsneikex  44204  clsneinex  44205  neicvgmex  44215  neicvgel1  44217  suprleubrd  44264  suprlubrd  44266  imo72b2  44270  dvconstbi  44432  bcc0  44438  binomcxplemnotnn0  44454  nnfoctb  45150  infleinflem1  45473  fprodcnlem  45704  sumnnodd  45735  icccncfext  45990  itgsin0pilem1  46053  stoweidlem32  46135  stoweidlem35  46138  stoweidlem36  46139  stoweidlem37  46140  stoweidlem43  46146  stoweidlem50  46153  wallispilem5  46172  stirlinglem2  46178  stirlinglem3  46179  stirlinglem4  46180  stirlinglem8  46184  stirlinglem11  46187  stirlinglem12  46188  stirlinglem14  46190  stirlinglem15  46191  fourierdlem11  46221  fourierdlem20  46230  fourierdlem21  46231  fourierdlem41  46251  fourierdlem42  46252  fourierdlem48  46257  fourierdlem49  46258  fourierdlem64  46273  fourierdlem71  46280  fourierdlem79  46288  fourierdlem90  46299  fourierdlem91  46300  fourierswlem  46333  etransclem17  46354  etransclem38  46375  saluni  46428  meaiininclem  46589  issmflelem  46847  issmfgtlem  46858  issmfgelem  46872  smflimsuplem4  46926  f1cof1blem  47179  zplusmodne  47448  m1modne  47453  submodneaddmod  47456  sprval  47584  prprval  47619  bgoldbtbndlem2  47911  bgoldbtbndlem3  47912  bgoldbtbnd  47914  isubgrvtxuhgr  47969  isubgredg  47971  grimcnv  47993  isuspgrim  48001  gricushgr  48022  uhgrimisgrgric  48036  grtriclwlk3  48050  isubgr3stgrlem7  48077  grlimgrtri  48108  grlictr  48120  gpgvtx0  48158  gpgvtx1  48159  gpgprismgrusgra  48163  gpgedgvtx1  48167  gpg3kgrtriex  48194  pgnbgreunbgrlem3  48223  pgnbgreunbgrlem6  48229  isclintop  48312  clintopcllaw  48316  nzrneg1ne0  48335  lidldomn1  48336  zlidlring  48339  uzlidlring  48340  2zrngnmlid  48360  cznrng  48366  coe1id  48490  blenre  48680  blennn  48681  2arymaptf  48758  itcoval1  48769  itcovalendof  48775  ehl2eudisval0  48831  eenglngeehlnmlem2  48844  itsclc0yqsol  48870  inlinecirc02plem  48892  ipolub  49093  ipoglb  49096  nelsubclem  49173  imaid  49260  imaf1co  49261  uptri  49320  uptrar  49322  uptrai  49323  oppc1stflem  49393  setrec2mpt  49803