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  1459  mpd3an3  1491  elabd2  3623  eueq2  3667  csbiegf  3879  difsnb  4768  reusv3i  5365  frpoinsg  6335  fimadmfo  6793  fimadmfoALT  6795  fvtresfn  6984  fvmpt3  6986  ffvelcdmd  7073  fnressn  7150  fsnex  7279  f1oiso2  7348  riota5f  7393  onsuc  7807  onsucuni  7822  frrlem10  8291  seqomlem2  8439  oaordi  8532  nnaordi  8605  qsdisj  8793  dom2lem  8997  canth2g  9128  limenpsi  9149  nnfi  9161  php4  9203  onfin  9208  sucxpdom  9230  dmfi  9302  fiin  9392  supiso  9446  ordiso2  9487  wdom2d  9552  elirrvOLD  9570  infeq5  9616  cantnfp1lem3  9659  cantnflem1d  9667  rankwflemb  9775  onenon  10001  cardonle  10009  sdomsdomcardi  10023  acni  10095  cardaleph  10139  djuen  10219  djuinf  10238  infdju1  10239  nnadju  10247  pwsdompw  10252  infdif  10257  cfval  10295  fin34  10439  fin1a2lem1  10449  fin1a2  10464  ttukeylem6  10563  sdomsdomcard  10615  canth3  10616  fpwwe2  10699  canthwelem  10706  gchdju1  10712  pwfseqlem4  10718  gchdjuidm  10724  gchxpidm  10725  tskwe2  10829  rankcf  10833  tskuni  10839  gruxp  10863  dmrecnq  11024  lterpq  11026  archnq  11036  reclem3pr  11105  reclem4pr  11106  0idsr  11153  lep1  12127  ledivp1  12188  negfi  12235  supaddc  12253  supmul1  12255  suprzcl  12748  uz11  12959  zmin  13040  zbtwnre  13042  rpnnen1lem4  13077  rpnnen1lem5  13078  xnegid  13337  supxrre  13426  infxrre  13436  eluzfz2  13633  fzsuc  13673  fzsuc2  13684  fzp1disj  13685  fzneuz  13710  nn0p1elfzo  13805  fllep1  13909  fraclt1  13910  fracle1  13911  fracge0  13912  flhalf  13938  ceige  13952  ceim1l  13955  fldiv  13968  modval  13979  suppssfz  14105  seqeq1  14115  expubnd  14289  iexpcyc  14318  binom2sub1  14332  faclbnd4lem3  14406  pfxid  14801  pfxccatpfx2  14853  swrdccat3blem  14855  cshw0  14912  cshwn  14915  cshimadifsn  14947  cshimadifsn0  14948  pfx2  15065  trclexlem  15114  shftfval  15190  shftcan1  15203  sgnneg  15220  reval  15240  cjmulrcl  15278  addcj  15282  absval  15372  absneg  15411  abscj  15413  sqabsadd  15416  sqabssub  15417  leabs  15433  sqreulem  15494  lo1res  15693  o1of2  15747  o1rlimmul  15753  fsumconst1  15924  flo1  15990  trirecip  15999  efcan  16229  efi4p  16272  resin4p  16273  recos4p  16274  sincossq  16311  ruclem10  16374  iddvds  16406  1dvds  16407  2ebits  16584  lcmftp  16773  coprmgcdb  16786  1idssfct  16817  exprmfct  16842  eulerthlem2  16920  odzphi  16935  pcprendvds  16979  pcmpt  17031  oddprmdvds  17042  vdwlem8  17127  0ram2  17160  prmgaplem7  17196  setsn0fun  17312  setsexstruct2  17314  pwsvscaval  17628  2initoinv  18146  initoeu1  18147  initoeu2lem1  18150  initoeu2  18152  2termoinv  18153  termoeu1  18154  homarel  18172  joinfval  18506  meetfval  18520  latjcom  18582  latmcom  18598  0subm  18974  sgrp2nmndlem5  19089  grprcan  19145  isgrpid2  19148  grpinvid  19171  mulgnn0z  19272  qus0  19365  eqg0subg  19372  ghmker  19417  symgbasmap  19552  symginv  19577  pmtrfrn  19633  odmulg2  19730  slwpgp  19788  pj1eq  19875  efgtf  19897  frgpinv  19939  frgpup2  19951  cnaddablx  20043  cnaddabl  20044  zaddablx  20047  imasabl  20051  dprdfadd  20197  dpjidcl  20235  dpjlid  20238  pgpfac1lem3  20254  omndmul2  20308  omndmul  20310  rngen1zr0  20367  srgen1zr0  20403  1unit  20565  unitgrpid  20576  1rinv  20586  irredn0  20614  irredneg  20621  c0snmgmhm  20653  rngisomring1  20659  zrrnghm  20749  rnrhmsubrg  20818  zrinitorngc  20855  zrtermorngc  20856  zrtermoringc  20888  isdrng2  20958  abv0  21041  abv1z  21042  abvneg  21044  orng0le1  21092  lmodfopne  21136  lsssn0  21184  lspsn0  21244  lsp0  21245  lmhmvsca  21281  lmhmrnlss  21286  lmhmkerlss  21287  lsppratlem5  21390  rsp1  21481  kerlidl  21533  ring2idlqus  21566  rngqiprngfulem4  21571  rngqiprngfu  21574  ssdifidllem  21601  cnfldneg  21665  zringcyg  21736  chrid  21792  chrrhm  21798  ip0r  21904  ocvlss  21939  ocv1  21946  rlmassa  22139  psrbagfsupp  22188  snifpsrbag  22189  psrbaglefi  22195  psrvscaval  22219  psrdi  22233  psrdir  22234  mplvscaval  22284  mhpmpl  22426  mhpdeg  22427  mhppwdeg  22432  psdmul  22448  psdpw  22452  coe1sclmulfv  22563  coe1id  22573  evl1var  22615  mamuvs1  22681  mamuvs2  22682  matecl  22701  matvscacell  22712  mat0scmat  22814  submaval0  22856  mdetrsca  22879  maduval  22914  minmar1val0  22923  pmatcollpw3fi1lem2  23066  chcoeffeqlem  23164  cayleyhamilton0  23168  cayleyhamiltonALT  23170  toponsspwpw  23201  cctop  23285  cldval  23302  ntrfval  23303  clsfval  23304  cmclsopn  23341  opncldf3  23365  neifval  23378  lpfval  23417  cnrmnrm  23640  dis2ndc  23740  islocfin  23797  tx1cn  23889  idqtop  23986  kqtopon  24007  kqid  24008  kqcld  24015  hmphen2  24079  filssufil  24192  ufileu  24199  alexsublem  24324  efmndtmd  24381  symgtgp  24386  ustuqtop4  24524  cstucnd  24563  metustexhalf  24836  nm0  24909  rlmnlm  24968  nmolb  24997  metdseq0  25135  pi1xfrval  25336  clmvneg1  25381  clmvsubval  25391  ipcau2  25516  tcphcphlem1  25517  tcphcphlem2  25518  cmetcaulem  25570  ovolicc2lem3  25801  ovolicc2lem4  25802  mbfmulc2lem  25929  i1fpos  25988  mbfi1fseqlem3  25999  itg2ge0  26017  bddiblnc  26123  dvres2  26193  dvaddbr  26219  dvmulbr  26220  dvcobr  26227  dvfsumlem4  26310  ftc1a  26318  ftc1lem6  26322  uc1pmon1p  26431  ig1pval2  26456  dgradd2  26548  dgrcolem2  26554  plydivlem4  26580  plydiveu  26582  rnplynfin  26593  elqaalem3  26607  qaa  26610  ulmdvlem1  26690  abelthlem6  26726  abelthlem7  26728  eflogeq  26893  jensenlem2  27278  harmonicbnd4  27301  sgmnncl  27437  dchrptlem2  27555  1lgs  27630  lgs1  27631  2sqcoprm  27725  addsqnreup  27733  dchrisumlem2  27780  dchrisum0lem2a  27807  selberg2lem  27840  pntrsumo1  27855  pntrsumbnd  27856  pntpbnd1  27876  pntlemr  27892  pntlemj  27893  padicabvf  27921  bdayval  27938  noextendgt  27960  nosupbnd2lem1  28005  noinfbnd2lem1  28020  noetainflem4  28030  oldval  28153  divmuls  28540  divscl  28542  seqsp1  28630  bdayfinbndlem1  28786  zz12s  28794  remulscllem1  28819  symquadprlnglem  29098  plngrotlem2  29199  tgaaddcpbllem1  29282  incistruhgr  29590  subgrprop3  29790  subgruhgredgd  29798  usgrexi  29955  cusgrexi  29957  cusgrsizeinds  29966  vtxdgfusgrf  30011  1hevtxdg1  30020  1egrvtxdg1  30023  ewlkprop  30117  wlklenvm1  30135  wlkl1loop  30151  wlkp1lem4  30188  2pthnloop  30250  upgrclwlkcompim  30301  crctcshwlkn0lem4  30335  crctcshwlkn0lem5  30336  crctcshwlkn0lem6  30337  crctcshwlkn0lem7  30338  crctcshlem4  30342  wspthnonp  30381  wlkswwlksf1o  30401  wwlksnwwlksnon  30437  umgr2wlkon  30472  wwlks2onv  30475  elwwlks2ons3im  30476  elwspths2spth  30492  umgrclwwlkge2  30515  clwlkclwwlkf1lem3  30530  erclwwlkref  30544  clwwlknp  30561  wwlksext2clwwlk  30581  wwlksubclwwlk  30582  0pthon1  30652  1wlkdlem4  30664  1pthd  30667  3spthd  30710  eupth2eucrct  30751  eucrctshift  30777  eucrct2eupth  30779  frgrncvvdeqlem8  30840  frgr2wwlkeqm  30865  isgrpoi  31033  grpoinvfval  31057  grpodivfval  31069  vcz  31110  cnaddabloOLD  31116  nvz0  31203  sspz  31270  lno0  31291  nmobndi  31310  ipasslem2  31367  shunssi  31903  ococin  31943  ssjo  31982  pjocini  32233  nlfnval  32416  lncnopbd  32572  riesz3i  32597  cnlnadjlem7  32608  pjclem4  32734  pj3si  32742  hstoc  32757  hstnmoc  32758  hstoh  32767  hst0  32768  mdsl2i  32857  chirredlem3  32927  chirredlem4  32928  dmdbr5ati  32957  rexunirn  33021  fcnvgreu  33199  infxrge0glb  33290  cycpmco2lem5  33624  cycpmco2lem6  33625  cycpmco2lem7  33626  isarchi3  33681  rlocisunit  33770  nsgqusf1olem2  33898  ssmxidllem  33931  rprmdvdspow  33998  ressply1sub  34035  selvply1rhmlemb  34084  fedgmullem1  34194  extdg1id  34231  nn0constr  34326  zartopn  34440  zarcmplem  34446  esumcvg  34651  esumcvgre  34656  sigaval  34676  unelldsys  34724  fiunelros  34740  measval  34764  pmeasmono  34890  probfinmeasb  34994  ballotlemfc0  35059  ballotlemfcc  35060  ballotlemsi  35081  ballotlemfrci  35094  signlem0  35150  breprexp  35196  bnj1006  35524  bnj1110  35546  bnj1253  35581  bnj1280  35584  bnj1463  35619  bnj1312  35622  scottrankeqel  35678  fineqvinfep  35718  erdszelem7  35883  erdszelem8  35884  cvmliftlem10  35980  cvmliftlem13  35982  cvmlift2lem9  35997  cvmlift3lem6  36010  cvmlift3lem7  36011  cvmlift3lem9  36013  satfv1lem  36048  dfrdg2  36479  cldregopn  37041  tailfval  37082  filnetlem3  37090  filnetlem4  37091  ontopbas  37138  bj-nnfbd  37593  bj-elid4  38009  bj-imdiridlem  38026  f1omptsnlem  38179  icoreunrn  38202  relowlpssretop  38207  fvineqsnf1  38253  wl-sbal2  38416  unccur  38446  poimirlem1  38459  poimirlem2  38460  poimirlem4  38462  poimirlem6  38464  poimirlem7  38465  poimirlem11  38469  poimirlem12  38470  poimirlem17  38475  poimirlem20  38478  poimirlem22  38480  poimirlem23  38481  poimirlem28  38486  poimir  38491  ismblfin  38499  cnambfre  38506  ftc1cnnc  38530  dvasin  38542  ismtyres  38662  heiborlem8  38672  ghomidOLD  38743  rngosn6  38780  rngonegmn1l  38795  rngonegmn1r  38796  rngoneglmul  38797  rngonegrmul  38798  idlnegcl  38876  0idl  38879  0rngo  38881  smprngopr  38906  sucmapsuc  39341  cossex  39361  qsdisjALTV  39551  cnvepresdmqss  39589  mpets2  39807  lkrval  40065  ldualvaddval  40108  ldualvsval  40115  opoc1  40179  pmap0  40742  pmap1N  40744  pexmidALTN  40955  cdleme31fv  41367  cdlemg27b  41673  erngdvlem4  41968  erng0g  41971  erngdvlem4-rN  41976  dvalveclem  42002  dvh0g  42088  dih0cnv  42260  dih1rn  42264  dih1cnv  42265  doch0  42335  doch1  42336  lcfl7lem  42476  mapdheq  42705  hdmap1eq  42778  hdmapval2lem  42808  hgmapvvlem3  42902  zndvdchrrhm  42943  lcmineqlem13  43011  aks4d1p9  43058  primrootsunit1  43067  aks6d1c1p1  43077  aks6d1c1p6  43084  aks6d1c1p8  43085  sticksstones1  43116  sticksstones6  43121  sticksstones7  43122  sticksstones11  43126  sticksstones12a  43127  sticksstones12  43128  sticksstones22  43138  aks6d1c6isolem1  43144  aks6d1c6isolem2  43145  unitscyglem5  43169  renegid  43352  sn-0ne2  43385  remul01  43386  remulinvcom  43412  sn-0tie0  43443  renegmulnnass  43457  domnexpgn0cl  43509  abvexp  43518  frlmsnic  43526  fsuppssind  43543  mzpval  43681  mzpindd  43695  pellex  43780  2nn0ind  43890  jm2.26lem3  43946  pw2f1o2val  43984  wepwsolem  43987  fnwe2lem3  43997  lnmfg  44027  dgrsub2  44080  mpaaeu  44095  flcidc  44115  dflim5  44274  naddwordnexlem1  44342  rtrclexlem  44560  cnvrcl0  44569  brcoffn  44974  clsk1indlem3  44987  clsneif1o  45048  clsneicnv  45049  clsneikex  45050  clsneinex  45051  neicvgmex  45061  neicvgel1  45063  suprleubrd  45110  suprlubrd  45112  imo72b2  45116  dvconstbi  45262  bcc0  45268  binomcxplemnotnn0  45284  nnfoctb  45986  infleinflem1  46303  fprodcnlem  46533  sumnnodd  46564  icccncfext  46819  itgsin0pilem1  46882  stoweidlem32  46964  stoweidlem35  46967  stoweidlem36  46968  stoweidlem37  46969  stoweidlem43  46975  stoweidlem50  46982  wallispilem5  47001  stirlinglem2  47007  stirlinglem3  47008  stirlinglem4  47009  stirlinglem8  47013  stirlinglem11  47016  stirlinglem12  47017  stirlinglem14  47019  stirlinglem15  47020  fourierdlem11  47050  fourierdlem20  47059  fourierdlem21  47060  fourierdlem41  47080  fourierdlem42  47081  fourierdlem48  47086  fourierdlem49  47087  fourierdlem64  47102  fourierdlem71  47109  fourierdlem79  47117  fourierdlem90  47128  fourierdlem91  47129  fourierswlem  47162  etransclem17  47183  etransclem38  47204  saluni  47257  meaiininclem  47418  issmflelem  47676  issmfgtlem  47687  issmfgelem  47701  smflimsuplem4  47755  sqrtnnaa  47835  f1cof1blem  48066  zplusmodne  48341  m1modne  48346  submodneaddmod  48349  nndivides2  48376  sprval  48483  prprval  48518  bgoldbtbndlem2  48826  bgoldbtbndlem3  48827  bgoldbtbnd  48829  isubgrvtxuhgr  48884  isubgredg  48886  grimcnv  48908  isuspgrim  48916  gricushgr  48937  uhgrimisgrgric  48951  grtriclwlk3  48965  isubgr3stgrlem7  48992  grlimgrtri  49023  grlictr  49035  gpgvtx0  49073  gpgvtx1  49074  gpgprismgrusgra  49078  gpgedgvtx1  49082  gpg3kgrtriex  49109  pgnbgreunbgrlem3  49138  pgnbgreunbgrlem6  49144  isclintop  49226  clintopcllaw  49230  nzrneg1ne0  49249  lidldomn1  49250  zlidlring  49253  uzlidlring  49254  2zrngnmlid  49274  cznrng  49280  blenre  49608  blennn  49609  2arymaptf  49686  itcoval1  49697  itcovalendof  49703  ehl2eudisval0  49759  eenglngeehlnmlem2  49772  itsclc0yqsol  49798  inlinecirc02plem  49820  ipolub  50018  ipoglb  50021  nelsubclem  50097  imaid  50184  imaf1co  50185  uptri  50244  uptrar  50246  uptrai  50247  oppc1stflem  50317  setrec2mpt  50712