Theorem simp2 998

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 994	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  simpl2  1001  simpr2  1004  simp2i  1007  simp2d  1010  simp12  1028  simp22  1031  simp32  1034  syld3an3  1283  3ianorr  1309  stoic4b  1433  nlim0  4395  tfisi  4587  sotri2  5027  sotri3  5028  feq123  5358  sefvex  5537  fvmptt  5608  fnfvima  5752  cocan1  5788  cocan2  5789  ovexg  5909  ovmpox  6003  ovmpoga  6004  caovimo  6068  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfrcllembxssdm  6357  tfrcllembfn  6358  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecrdg  6409  mapxpen  6848  dif1en  6879  diffifi  6894  unsnfidcex  6919  unfidisj  6921  undifdc  6923  resfnfinfinss  6939  funrnfi  6941  sbthlemi9  6964  elfir  6972  difinfsn  7099  ctssdc  7112  djuassen  7216  xpdjuen  7217  mulcanenq  7384  ltanqg  7399  mulcanenq0ec  7444  addnnnq0  7448  distrprg  7587  aptipr  7640  addsrpr  7744  mulsrpr  7745  mulasssrg  7757  ltpsrprg  7802  axmulass  7872  axpre-ltadd  7885  subadd2  8161  nppcan  8179  nppcan3  8181  subsub2  8185  subsub4  8190  npncan3  8195  pnpcan  8196  pnncan  8198  subcan  8212  ltadd1  8386  leadd1  8387  leadd2  8388  ltsubadd  8389  ltsubadd2  8390  lesubadd  8391  lesubadd2  8392  ltaddsub  8393  leaddsub  8395  lesub1  8413  lesub2  8414  ltsub1  8415  ltsub2  8416  gt0add  8530  apreap  8544  lemul1  8550  reapmul1lem  8551  reapmul1  8552  reapadd1  8553  remulext1  8556  remulext2  8557  apadd2  8566  mulext2  8570  mulap0r  8572  leltap  8582  ltap  8590  apsub1  8599  recexaplem2  8609  mulcanap  8622  mulcanap2  8623  divvalap  8631  divmulap  8632  divcanap1  8638  diveqap0  8639  divap0b  8640  divrecap  8645  divassap  8647  div23ap  8648  divdirap  8654  divcanap3  8655  div11ap  8657  diveqap1  8662  divmuldivap  8669  divcanap5  8671  redivclap  8688  div2negap  8692  apmul1  8745  apmul2  8746  div2subap  8794  ltdiv1  8825  ledivmul  8834  lemuldiv  8838  lt2msq1  8842  ltdiv23  8849  squeeze0  8861  zaddcllemneg  9292  eluzsub  9557  nn01to3  9617  rpgecl  9682  addlelt  9768  xleadd1  9875  xltadd1  9876  lbioog  9913  ubioc1  9929  ubicc2  9985  icoshftf1o  9991  fzen  10043  ubmelfzo  10200  ssfzo12  10224  ubmelm1fzo  10226  fzosplitprm1  10234  rebtwn2zlemshrink  10254  qbtwnre  10257  icogelb  10266  flqwordi  10288  flqword2  10289  flltdivnn0lt  10304  modqcl  10326  mulqmod0  10330  modqmulnn  10342  modqabs2  10358  modqmuladdnn0  10368  qnegmod  10369  addmodid  10372  modqm1p1mod0  10375  modifeq2int  10386  modqdi  10392  modqeqmodmin  10394  modfzo0difsn  10395  frec2uzf1od  10406  exp3val  10522  expnegap0  10528  expgt1  10558  exprecap  10561  expmulzap  10566  leexp2a  10573  expubnd  10577  mulbinom2  10637  bernneq2  10642  expnbnd  10644  fihashss  10796  fihashssdif  10798  fimaxq  10807  shftuz  10826  shftfibg  10829  cjdivap  10918  resqrtcl  11038  absdivap  11079  abssubne0  11100  maxleast  11222  lemininf  11242  ltmininf  11243  xrmaxltsup  11266  xrmaxaddlem  11268  xrmaxadd  11269  xrmineqinf  11277  xrltmininf  11278  xrminltinf  11280  xrminadd  11283  climuni  11301  reccn2ap  11321  isumz  11397  geoisum1c  11528  prod1dc  11594  efltim  11706  dvdsval2  11797  dvdscmulr  11827  dvdsmulcr  11828  modmulconst  11830  dvdsadd2b  11847  dvdsexp  11867  mulmoddvds  11869  divalglemeuneg  11928  zsupssdc  11955  gcdaddm  11985  dvdsgcdb  12014  mulgcd  12017  gcddiv  12020  uzwodc  12038  lcmdvdsb  12084  mulgcddvds  12094  qredeq  12096  divgcdcoprm0  12101  cncongr1  12103  euclemma  12146  rpexp  12153  rpexp12i  12155  fermltl  12234  prmdiv  12235  odzcllem  12242  odzdvds  12245  odzphi  12246  vfermltl  12251  coprimeprodsq  12257  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem12  12275  pythagtriplem13  12276  pceu  12295  pcdvdsb  12319  pcgcd1  12327  dvdsprmpweq  12334  sumhashdc  12345  ctinf  12431  fvsetsid  12496  ressressg  12534  ressabsg  12535  rngplusgg  12595  imasaddvallemg  12736  qusaddvallemg  12752  plusfvalg  12782  mgmb1mgm1  12787  issubmnd  12843  ress0g  12844  grpasscan2  12934  grpidrcan  12935  grpidlcan  12936  grpinvadd  12948  grpsubeq0  12956  grppncan  12961  dfgrp3mlem  12968  dfgrp3me  12970  grpsubpropd2  12975  mhmmnd  12980  mulgnn0p1  12994  mulgnnsubcl  12995  mulgnn0subcl  12996  mulgsubcl  12997  mulgneg  13001  mulgaddcom  13007  mulginvcom  13008  subgcl  13044  subgsubcl  13045  subgsub  13046  subgmulg  13048  nsgconj  13066  nsgid  13075  ablinvadd  13113  ablsub4  13116  ablpncan2  13119  srgcl  13153  ringcl  13196  crngcom  13197  ringidss  13212  ringcom  13214  opprringbg  13250  unitmulcl  13282  unitmulclb  13283  dvrcl  13304  unitdvcl  13305  dvrcan1  13309  dvrcan3  13310  subrgmcl  13354  subrgdv  13359  islmod  13381  scafvalg  13397  lmodcom  13423  rmodislmodlem  13440  rmodislmod  13441  2basgeng  13585  iuncld  13618  ntrss  13622  restco  13677  restabs  13678  cnprcl2k  13709  lmconst  13719  cnrest2  13739  cnmpt2t  13796  psmetsym  13832  psmetge0  13834  xmetge0  13868  xmetsym  13871  blvalps  13891  blval  13892  xblcntrps  13916  xblcntr  13917  xmssym  13972  blsscls2  13996  bdxmet  14004  txmetcnp  14021  dvfvalap  14153  dvid  14165  dvcnp2cntop  14166  rpcxpadd  14329  rpcxpsub  14332  rpmulcxp  14333  rpdivcxp  14335  cxpmul  14336  rpcxple2  14341  rpcxplt2  14342  rplogbval  14366  rplogbcl  14367  rplogbreexp  14374  relogbexpap  14379  logbleb  14382  logblt  14383  rplogbcxp  14384  rpcxplogb  14385  relogbcxpbap  14386  lgsneg1  14429  lgsmod  14430  lgsne0  14442  lgssq  14444  lgsdirnn0  14451  lgsdinn0  14452  findset  14700