Theorem simp2 1000

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)

Proof of Theorem simp2

Step	Hyp	Ref	Expression
1		3simpa 996	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simpl2  1003  simpr2  1006  simp2i  1009  simp2d  1012  simp12  1030  simp22  1033  simp32  1036  syld3an3  1294  3ianorr  1320  stoic4b  1444  nlim0  4430  tfisi  4624  sotri2  5068  sotri3  5069  feq123  5402  sefvex  5582  fvmptt  5656  fnfvima  5800  cocan1  5837  cocan2  5838  ovexg  5959  ovmpox  6055  ovmpoga  6056  fvmpopr2d  6063  caovimo  6121  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfrcllembxssdm  6423  tfrcllembfn  6424  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecrdg  6475  mapxpen  6918  dif1en  6949  diffifi  6964  unsnfidcex  6990  unfidisj  6992  undifdc  6994  resfnfinfinss  7014  funrnfi  7017  sbthlemi9  7040  elfir  7048  difinfsn  7175  ctssdc  7188  djuassen  7302  xpdjuen  7303  mulcanenq  7471  ltanqg  7486  mulcanenq0ec  7531  addnnnq0  7535  distrprg  7674  aptipr  7727  addsrpr  7831  mulsrpr  7832  mulasssrg  7844  ltpsrprg  7889  axmulass  7959  axpre-ltadd  7972  subadd2  8249  nppcan  8267  nppcan3  8269  subsub2  8273  subsub4  8278  npncan3  8283  pnpcan  8284  pnncan  8286  subcan  8300  ltadd1  8475  leadd1  8476  leadd2  8477  ltsubadd  8478  ltsubadd2  8479  lesubadd  8480  lesubadd2  8481  ltaddsub  8482  leaddsub  8484  lesub1  8502  lesub2  8503  ltsub1  8504  ltsub2  8505  gt0add  8619  apreap  8633  lemul1  8639  reapmul1lem  8640  reapmul1  8641  reapadd1  8642  remulext1  8645  remulext2  8646  apadd2  8655  mulext2  8659  mulap0r  8661  leltap  8671  ltap  8679  apsub1  8688  recexaplem2  8698  mulcanap  8711  mulcanap2  8712  divvalap  8720  divmulap  8721  divcanap1  8727  diveqap0  8728  divap0b  8729  divrecap  8734  divassap  8736  div23ap  8737  divdirap  8743  divcanap3  8744  div11ap  8746  diveqap1  8751  divmuldivap  8758  divcanap5  8760  redivclap  8777  div2negap  8781  apmul1  8834  apmul2  8835  div2subap  8883  ltdiv1  8914  ledivmul  8923  lemuldiv  8927  lt2msq1  8931  ltdiv23  8938  squeeze0  8950  ofnegsub  9008  zaddcllemneg  9384  eluzsub  9650  nn01to3  9710  rpgecl  9776  addlelt  9862  xleadd1  9969  xltadd1  9970  lbioog  10007  ubioc1  10023  ubicc2  10079  icoshftf1o  10085  fzen  10137  nelfzo  10246  ubmelfzo  10295  ssfzo12  10319  ubmelm1fzo  10321  fzosplitprm1  10329  zsupssdc  10347  rebtwn2zlemshrink  10362  qbtwnre  10365  icogelb  10374  flqwordi  10397  flqword2  10398  flltdivnn0lt  10413  modqcl  10437  mulqmod0  10441  modqmulnn  10453  modqabs2  10469  modqmuladdnn0  10479  qnegmod  10480  addmodid  10483  modqm1p1mod0  10486  modifeq2int  10497  modqdi  10503  modqeqmodmin  10505  modfzo0difsn  10506  frec2uzf1od  10517  exp3val  10652  expnegap0  10658  expgt1  10688  exprecap  10691  expmulzap  10696  leexp2a  10703  expubnd  10707  mulbinom2  10767  bernneq2  10772  expnbnd  10774  fihashss  10927  fihashssdif  10929  fimaxq  10938  shftuz  11001  shftfibg  11004  cjdivap  11093  resqrtcl  11213  absdivap  11254  abssubne0  11275  maxleast  11397  lemininf  11418  ltmininf  11419  xrmaxltsup  11442  xrmaxaddlem  11444  xrmaxadd  11445  xrmineqinf  11453  xrltmininf  11454  xrminltinf  11456  xrminadd  11459  climuni  11477  reccn2ap  11497  isumz  11573  geoisum1c  11704  prod1dc  11770  efltim  11882  dvdsval2  11974  dvdscmulr  12004  dvdsmulcr  12005  modmulconst  12007  dvdsadd2b  12024  dvdsexp  12045  mulmoddvds  12047  divalglemeuneg  12107  gcdaddm  12178  dvdsgcdb  12207  mulgcd  12210  gcddiv  12213  uzwodc  12231  lcmdvdsb  12279  mulgcddvds  12289  qredeq  12291  divgcdcoprm0  12296  cncongr1  12298  euclemma  12341  rpexp  12348  rpexp12i  12350  fermltl  12429  prmdiv  12430  odzcllem  12438  odzdvds  12441  odzphi  12442  vfermltl  12447  coprimeprodsq  12453  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem12  12471  pythagtriplem13  12472  pceu  12491  pcdvdsb  12516  pcgcd1  12524  dvdsprmpweq  12531  sumhashdc  12543  ctinf  12674  fvsetsid  12739  ressressg  12780  ressabsg  12781  rngplusgg  12841  imasaddvallemg  13019  qusaddvallemg  13037  plusfvalg  13067  mgmb1mgm1  13072  issubmnd  13146  ress0g  13147  imasmnd2  13156  imasmnd  13157  gsumfzz  13199  grpasscan2  13268  grpidrcan  13269  grpidlcan  13270  grpinvadd  13282  grpsubeq0  13290  grppncan  13295  dfgrp3mlem  13302  dfgrp3me  13304  grpsubpropd2  13309  pwsinvg  13316  imasgrp2  13318  imasgrp  13319  mhmmnd  13324  mulgnn0p1  13341  mulgnnsubcl  13342  mulgnn0subcl  13343  mulgsubcl  13344  mulgneg  13348  mulgaddcom  13354  mulginvcom  13355  submmulg  13374  subgcl  13392  subgsubcl  13393  subgsub  13394  subgmulg  13396  nsgconj  13414  nsgid  13423  quseccl0g  13439  ghmmulg  13464  ghmeqker  13479  f1ghm0to0  13480  kerf1ghm  13482  ablinvadd  13518  ablsub4  13521  ablpncan2  13524  subgabl  13540  gsumfzconst  13549  rngcl  13578  imasrng  13590  srgcl  13604  ringcl  13647  crngcom  13648  ringidss  13663  ringcom  13665  imasring  13698  opprringbg  13714  unitmulcl  13747  unitmulclb  13748  dvrcl  13769  unitdvcl  13770  dvrcan1  13774  dvrcan3  13775  rhmmul  13798  subrngrng  13836  subrngmcl  13843  subrgmcl  13867  subrgdv  13872  rrgeq0  13899  domneq0  13906  islmod  13925  scafvalg  13941  lmodcom  13967  rmodislmodlem  13984  rmodislmod  13985  lssclg  13998  lssvnegcl  14010  lssintclm  14018  lspss  14033  lspun  14036  lspsnvsi  14052  rspssp  14128  rnglidlmmgm  14130  rnglidlmsgrp  14131  rnglidlrng  14132  zndvds  14283  2basgeng  14426  iuncld  14459  ntrss  14463  restco  14518  restabs  14519  cnprcl2k  14550  lmconst  14560  cnrest2  14580  cnmpt2t  14637  psmetsym  14673  psmetge0  14675  xmetge0  14709  xmetsym  14712  blvalps  14732  blval  14733  xblcntrps  14757  xblcntr  14758  xmssym  14813  blsscls2  14837  bdxmet  14845  txmetcnp  14862  dvfvalap  15025  dvid  15039  dvidre  15041  dvcnp2cntop  15043  elplyr  15084  rpcxpadd  15249  rpcxpsub  15252  rpmulcxp  15253  rpdivcxp  15255  cxpmul  15256  rpcxple2  15262  rpcxplt2  15263  rplogbval  15289  rplogbcl  15290  rplogbreexp  15297  relogbexpap  15302  logbleb  15305  logblt  15306  rplogbcxp  15307  rpcxplogb  15308  relogbcxpbap  15309  sgmppw  15336  lgsneg1  15374  lgsmod  15375  lgsne0  15387  lgssq  15389  lgsdirnn0  15396  lgsdinn0  15397  lgsquad  15429  findset  15699