Theorem mpdan 700

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		mpdan.1	. 2 ⊢ (𝜑 → 𝜓)
3		mpdan.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpidan  702  mpan2  704  biadanid  835  mpjaodan  973  mpjao3dan  1460  mpd3an3  1492  elabd2  3627  eueq2  3671  csbiegf  3884  difsnb  4769  reusv3i  5370  frpoinsg  6364  fimadmfo  6827  fimadmfoALT  6829  fvtresfn  7019  fvmpt3  7021  ffvelcdmd  7109  fnressn  7186  fsnex  7314  f1oiso2  7383  riota5f  7428  onsuc  7848  onsucuni  7863  fnwe2lem4  8175  frrlem10  8341  seqomlem2  8489  oaordi  8582  nnaordi  8655  qsdisj  8843  dom2lem  9047  canth2g  9178  limenpsi  9199  nnfi  9211  php4  9253  onfin  9258  sucxpdom  9280  dmfi  9352  fiin  9441  supiso  9495  ordiso2  9536  wdom2d  9601  elirrvOLD  9619  infeq5  9665  cantnfp1lem3  9708  cantnflem1d  9716  rankwflemb  9827  rankwflembOLD  9828  onenon  10057  cardonle  10065  sdomsdomcardi  10079  acni  10151  cardaleph  10195  djuen  10275  djuinf  10294  infdju1  10295  nnadju  10303  pwsdompw  10308  infdif  10313  cfval  10351  fin34  10495  fin1a2lem1  10505  fin1a2  10520  ttukeylem6  10619  sdomsdomcard  10671  canth3  10672  fpwwe2  10755  canthwelem  10762  gchdju1  10768  pwfseqlem4  10774  gchdjuidm  10780  gchxpidm  10781  tskwe2  10885  rankcf  10889  tskuni  10895  gruxp  10919  dmrecnq  11080  lterpq  11082  archnq  11092  reclem3pr  11161  reclem4pr  11162  0idsr  11209  lep1  12185  ledivp1  12246  negfi  12293  supaddc  12311  supmul1  12313  suprzcl  12806  uz11  13017  zmin  13098  zbtwnre  13100  rpnnen1lem4  13135  rpnnen1lem5  13136  xnegid  13395  supxrre  13484  infxrre  13494  eluzfz2  13692  fzsuc  13732  fzsuc2  13743  fzp1disj  13744  fzneuz  13769  nn0p1elfzo  13864  fllep1  13968  fraclt1  13969  fracle1  13970  fracge0  13971  flhalf  13997  ceige  14011  ceim1l  14014  fldiv  14027  modval  14038  suppssfz  14164  seqeq1  14174  expubnd  14348  iexpcyc  14378  binom2sub1  14392  faclbnd4lem3  14466  pfxid  14862  pfxccatpfx2  14914  swrdccat3blem  14916  cshw0  14973  cshwn  14976  cshimadifsn  15008  cshimadifsn0  15009  pfx2  15127  trclexlem  15176  shftfval  15252  shftcan1  15265  sgnneg  15282  reval  15302  cjmulrcl  15340  addcj  15344  absval  15434  absneg  15473  abscj  15475  sqabsadd  15478  sqabssub  15479  leabs  15495  sqreulem  15556  lo1res  15755  o1of2  15809  o1rlimmul  15815  fsumconst1  15986  flo1  16052  trirecip  16061  efcan  16291  efi4p  16334  resin4p  16335  recos4p  16336  sincossq  16373  ruclem10  16436  iddvds  16468  1dvds  16469  2ebits  16646  lcmftp  16840  coprmgcdb  16853  1idssfct  16884  exprmfct  16909  eulerthlem2  16988  odzphi  17003  pcprendvds  17047  pcmpt  17099  oddprmdvds  17110  vdwlem8  17195  0ram2  17228  prmgaplem7  17264  setsn0fun  17380  setsexstruct2  17382  pwsvscaval  17696  2initoinv  18214  initoeu1  18215  initoeu2lem1  18218  initoeu2  18220  2termoinv  18221  termoeu1  18222  homarel  18240  joinfval  18574  meetfval  18588  latjcom  18650  latmcom  18666  0subm  19042  sgrp2nmndlem5  19157  grprcan  19213  isgrpid2  19216  grpinvid  19239  mulgnn0z  19340  qus0  19433  eqg0subg  19440  ghmker  19485  symgbasmap  19621  symginv  19646  pmtrfrn  19702  odmulg2  19799  slwpgp  19857  pj1eq  19944  efgtf  19966  frgpinv  20008  frgpup2  20020  cnaddablx  20112  cnaddabl  20113  zaddablx  20116  imasabl  20120  dprdfadd  20266  dpjidcl  20304  dpjlid  20307  pgpfac1lem3  20323  omndmul2  20377  omndmul  20379  rngen1zr0  20436  srgen1zr0  20472  1unit  20634  unitgrpid  20645  1rinv  20655  irredn0  20683  irredneg  20690  c0snmgmhm  20722  rngisomring1  20728  zrrnghm  20818  rnrhmsubrg  20887  zrinitorngc  20924  zrtermorngc  20925  zrtermoringc  20957  isdrng2  21027  abv0  21110  abv1z  21111  abvneg  21113  orng0le1  21161  lmodfopne  21205  lsssn0  21253  lspsn0  21313  lsp0  21314  lmhmvsca  21350  lmhmrnlss  21355  lmhmkerlss  21356  lsppratlem5  21459  rsp1  21550  kerlidl  21602  ring2idlqus  21635  rngqiprngfulem4  21640  rngqiprngfu  21643  ssdifidllem  21670  cnfldneg  21734  zringcyg  21805  chrid  21861  chrrhm  21867  ip0r  21973  ocvlss  22008  ocv1  22015  rlmassa  22208  psrbagfsupp  22257  snifpsrbag  22258  psrbaglefi  22264  psrvscaval  22288  psrdi  22302  psrdir  22303  mplvscaval  22353  mhpmpl  22495  mhpdeg  22496  mhppwdeg  22501  psdmul  22517  psdpw  22521  coe1sclmulfv  22632  coe1id  22642  evl1var  22684  mamuvs1  22750  mamuvs2  22751  matecl  22770  matvscacell  22781  mat0scmat  22883  submaval0  22925  mdetrsca  22948  maduval  22983  minmar1val0  22992  pmatcollpw3fi1lem2  23135  chcoeffeqlem  23233  cayleyhamilton0  23237  cayleyhamiltonALT  23239  toponsspwpw  23270  cctop  23354  cldval  23371  ntrfval  23372  clsfval  23373  cmclsopn  23410  opncldf3  23434  neifval  23447  lpfval  23486  cnrmnrm  23709  dis2ndc  23809  islocfin  23866  tx1cn  23958  idqtop  24055  kqtopon  24076  kqid  24077  kqcld  24084  hmphen2  24148  filssufil  24261  ufileu  24268  alexsublem  24393  efmndtmd  24450  symgtgp  24455  ustuqtop4  24593  cstucnd  24632  metustexhalf  24905  nm0  24978  rlmnlm  25037  nmolb  25066  metdseq0  25204  pi1xfrval  25405  clmvneg1  25450  clmvsubval  25460  ipcau2  25585  tcphcphlem1  25586  tcphcphlem2  25587  cmetcaulem  25639  ovolicc2lem3  25870  ovolicc2lem4  25871  mbfmulc2lem  25998  i1fpos  26057  mbfi1fseqlem3  26068  itg2ge0  26086  bddiblnc  26192  dvres2  26262  dvaddbr  26288  dvmulbr  26289  dvcobr  26296  dvfsumlem4  26379  ftc1a  26387  ftc1lem6  26391  uc1pmon1p  26500  ig1pval2  26525  dgradd2  26617  dgrcolem2  26623  plydivlem4  26647  plydiveu  26649  rnplynfin  26660  elqaalem3  26674  qaa  26677  ulmdvlem1  26757  abelthlem6  26793  abelthlem7  26795  eflogeq  26960  jensenlem2  27345  harmonicbnd4  27368  sgmnncl  27504  dchrptlem2  27622  1lgs  27697  lgs1  27698  2sqcoprm  27792  addsqnreup  27800  dchrisumlem2  27847  dchrisum0lem2a  27874  selberg2lem  27907  pntrsumo1  27922  pntrsumbnd  27923  pntpbnd1  27943  pntlemr  27959  pntlemj  27960  padicabvf  27988  bdayval  28035  noextendgt  28057  nosupbnd2lem1  28102  noinfbnd2lem1  28117  noetainflem4  28127  oldval  28250  divmuls  28637  divscl  28639  seqsp1  28727  bdayfinbndlem1  28883  zz12s  28891  remulscllem1  28916  symquadprlnglem  29195  plngrotlem2  29296  tgaaddcpbllem1  29379  incistruhgr  29687  subgrprop3  29887  subgruhgredgd  29895  usgrexi  30052  cusgrexi  30054  cusgrsizeinds  30063  vtxdgfusgrf  30108  1hevtxdg1  30117  1egrvtxdg1  30120  ewlkprop  30214  wlklenvm1  30232  wlkl1loop  30248  wlkp1lem4  30285  2pthnloop  30347  upgrclwlkcompim  30398  crctcshwlkn0lem4  30432  crctcshwlkn0lem5  30433  crctcshwlkn0lem6  30434  crctcshwlkn0lem7  30435  crctcshlem4  30439  wspthnonp  30478  wlkswwlksf1o  30498  wwlksnwwlksnon  30534  umgr2wlkon  30569  wwlks2onv  30572  elwwlks2ons3im  30573  elwspths2spth  30589  umgrclwwlkge2  30612  clwlkclwwlkf1lem3  30627  erclwwlkref  30641  clwwlknp  30658  wwlksext2clwwlk  30678  wwlksubclwwlk  30679  0pthon1  30749  1wlkdlem4  30761  1pthd  30764  3spthd  30807  eupth2eucrct  30848  eucrctshift  30874  eucrct2eupth  30876  frgrncvvdeqlem8  30937  frgr2wwlkeqm  30962  isgrpoi  31130  grpoinvfval  31154  grpodivfval  31166  vcz  31207  cnaddabloOLD  31213  nvz0  31300  sspz  31367  lno0  31388  nmobndi  31407  ipasslem2  31464  shunssi  32000  ococin  32040  ssjo  32079  pjocini  32330  nlfnval  32513  lncnopbd  32669  riesz3i  32694  cnlnadjlem7  32705  pjclem4  32831  pj3si  32839  hstoc  32854  hstnmoc  32855  hstoh  32864  hst0  32865  mdsl2i  32954  chirredlem3  33024  chirredlem4  33025  dmdbr5ati  33054  rexunirn  33160  fcnvgreu  33338  infxrge0glb  33427  cycpmco2lem5  33761  cycpmco2lem6  33762  cycpmco2lem7  33763  isarchi3  33818  rlocisunit  33907  nsgqusf1olem2  34035  ssmxidllem  34068  rprmdvdspow  34135  ressply1sub  34172  selvply1rhmlemb  34221  fedgmullem1  34331  extdg1id  34368  nn0constr  34463  zartopn  34577  zarcmplem  34583  esumcvg  34788  esumcvgre  34793  sigaval  34813  unelldsys  34861  fiunelros  34877  measval  34901  pmeasmono  35026  probfinmeasb  35130  ballotlemfc0  35195  ballotlemfcc  35196  ballotlemsi  35217  ballotlemfrci  35230  signlem0  35286  breprexp  35332  bnj1006  35660  bnj1110  35682  bnj1253  35717  bnj1280  35720  bnj1463  35755  bnj1312  35758  scottrankeqel  35832  fineqvinfep  35893  k3n0k1lt  36023  k3n0k2lt  36024  jltalephlem  36025  erdszelem7  36129  erdszelem8  36130  cvmliftlem10  36226  cvmliftlem13  36228  cvmlift2lem9  36243  cvmlift3lem6  36256  cvmlift3lem7  36257  cvmlift3lem9  36259  satfv1lem  36294  dfrdg2  36735  cldregopn  37297  tailfval  37338  filnetlem3  37346  filnetlem4  37347  ontopbas  37394  bj-nnfbd  37849  bj-elid4  38281  bj-imdiridlem  38298  f1omptsnlem  38451  icoreunrn  38474  relowlpssretop  38479  fvineqsnf1  38525  wl-sbal2  38688  unccur  38718  poimirlem1  38731  poimirlem2  38732  poimirlem4  38734  poimirlem6  38736  poimirlem7  38737  poimirlem11  38741  poimirlem12  38742  poimirlem17  38747  poimirlem20  38750  poimirlem22  38752  poimirlem23  38753  poimirlem28  38758  poimir  38763  ismblfin  38771  cnambfre  38778  ftc1cnnc  38802  dvasin  38814  ismtyres  38934  heiborlem8  38944  ghomidOLD  39015  rngosn6  39052  rngonegmn1l  39067  rngonegmn1r  39068  rngoneglmul  39069  rngonegrmul  39070  idlnegcl  39148  0idl  39151  0rngo  39153  smprngopr  39178  sucmapsuc  39613  cossex  39633  qsdisjALTV  39823  cnvepresdmqss  39861  mpets2  40079  lkrval  40337  ldualvaddval  40380  ldualvsval  40387  opoc1  40451  pmap0  41014  pmap1N  41016  pexmidALTN  41227  cdleme31fv  41639  cdlemg27b  41945  erngdvlem4  42240  erng0g  42243  erngdvlem4-rN  42248  dvalveclem  42274  dvh0g  42360  dih0cnv  42532  dih1rn  42536  dih1cnv  42537  doch0  42607  doch1  42608  lcfl7lem  42748  mapdheq  42977  hdmap1eq  43050  hdmapval2lem  43080  hgmapvvlem3  43174  zndvdchrrhm  43215  lcmineqlem13  43283  aks4d1p9  43330  primrootsunit1  43339  aks6d1c1p1  43349  aks6d1c1p6  43356  aks6d1c1p8  43357  sticksstones1  43388  sticksstones6  43393  sticksstones7  43394  sticksstones11  43398  sticksstones12a  43399  sticksstones12  43400  sticksstones22  43410  aks6d1c6isolem1  43416  aks6d1c6isolem2  43417  unitscyglem5  43441  renegid  43617  sn-0ne2  43650  remul01  43651  remulinvcom  43677  sn-0tie0  43708  renegmulnnass  43722  domnexpgn0cl  43777  abvexp  43789  frlmsnic  43797  fsuppssind  43814  mzpval  43936  mzpindd  43950  pellex  44035  2nn0ind  44145  jm2.26lem3  44201  pw2f1o2val  44239  wepwsolem  44242  lnmfg  44277  dgrsub2  44329  mpaaeu  44344  flcidc  44364  dflim5  44523  naddwordnexlem1  44591  rtrclexlem  44808  cnvrcl0  44817  brcoffn  45222  clsk1indlem3  45235  clsneif1o  45296  clsneicnv  45297  clsneikex  45298  clsneinex  45299  neicvgmex  45309  neicvgel1  45311  suprleubrd  45358  suprlubrd  45360  imo72b2  45364  dvconstbi  45510  bcc0  45516  binomcxplemnotnn0  45532  nnfoctb  46270  infleinflem1  46586  fprodcnlem  46816  sumnnodd  46847  icccncfext  47102  itgsin0pilem1  47165  stoweidlem32  47247  stoweidlem35  47250  stoweidlem36  47251  stoweidlem37  47252  stoweidlem43  47258  stoweidlem50  47265  wallispilem5  47284  stirlinglem2  47290  stirlinglem3  47291  stirlinglem4  47292  stirlinglem8  47296  stirlinglem11  47299  stirlinglem12  47300  stirlinglem14  47302  stirlinglem15  47303  fourierdlem11  47333  fourierdlem20  47342  fourierdlem21  47343  fourierdlem41  47363  fourierdlem42  47364  fourierdlem48  47369  fourierdlem49  47370  fourierdlem64  47385  fourierdlem71  47392  fourierdlem79  47400  fourierdlem90  47411  fourierdlem91  47412  fourierswlem  47445  etransclem17  47466  etransclem38  47487  saluni  47540  meaiininclem  47701  issmflelem  47959  issmfgtlem  47970  issmfgelem  47984  smflimsuplem4  48038  sqrtnnaa  48118  f1cof1blem  48349  zplusmodne  48624  m1modne  48629  submodneaddmod  48632  nndivides2  48659  sprval  48766  prprval  48801  bgoldbtbndlem2  49109  bgoldbtbndlem3  49110  bgoldbtbnd  49112  isubgrvtxuhgr  49167  isubgredg  49169  grimcnv  49191  isuspgrim  49199  gricushgr  49220  uhgrimisgrgric  49234  grtriclwlk3  49248  isubgr3stgrlem7  49275  grlimgrtri  49306  grlictr  49318  gpgvtx0  49356  gpgvtx1  49357  gpgprismgrusgra  49361  gpgedgvtx1  49365  gpg3kgrtriex  49392  pgnbgreunbgrlem3  49421  pgnbgreunbgrlem6  49427  isclintop  49509  clintopcllaw  49513  nzrneg1ne0  49532  lidldomn1  49533  zlidlring  49536  uzlidlring  49537  2zrngnmlid  49557  cznrng  49563  blenre  49891  blennn  49892  2arymaptf  49969  itcoval1  49980  itcovalendof  49986  ehl2eudisval0  50043  eenglngeehlnmlem2  50056  itsclc0yqsol  50081  inlinecirc02plem  50103  ipolub  50307  ipoglb  50310  nelsubclem  50386  imaid  50475  imaf1co  50476  uptri  50535  uptrar  50537  uptrai  50538  oppc1stflem  50614  setrec2mpt  51070