Theorem simp2 947

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

Syntax hints:   → wi 4   ∧ w3a 927

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

This theorem depends on definitions:  df-bi 116  df-3an 929

This theorem is referenced by:  simpl2  950  simpr2  953  simp2i  956  simp2d  959  simp12  977  simp22  980  simp32  983  syld3an3  1226  3ianorr  1252  stoic4b  1374  nlim0  4245  tfisi  4430  sotri2  4862  sotri3  4863  feq123  5187  sefvex  5361  fvmptt  5430  fnfvima  5568  cocan1  5604  cocan2  5605  ovexg  5721  ovmpt2x  5811  ovmpt2ga  5812  caovimo  5876  tfr1onlembxssdm  6146  tfr1onlembfn  6147  tfrcllembxssdm  6159  tfrcllembfn  6160  freccllem  6205  frecfcllem  6207  frecsuclem  6209  frecrdg  6211  mapxpen  6644  dif1en  6675  diffifi  6690  unsnfidcex  6710  unfidisj  6712  undifdc  6714  resfnfinfinss  6729  funrnfi  6731  sbthlemi9  6754  mulcanenq  7041  ltanqg  7056  mulcanenq0ec  7101  addnnnq0  7105  distrprg  7244  aptipr  7297  addsrpr  7388  mulsrpr  7389  mulasssrg  7401  axmulass  7505  axpre-ltadd  7518  subadd2  7783  nppcan  7801  nppcan3  7803  subsub2  7807  subsub4  7812  npncan3  7817  pnpcan  7818  pnncan  7820  subcan  7834  ltadd1  8004  leadd1  8005  leadd2  8006  ltsubadd  8007  ltsubadd2  8008  lesubadd  8009  lesubadd2  8010  ltaddsub  8011  leaddsub  8013  lesub1  8031  lesub2  8032  ltsub1  8033  ltsub2  8034  gt0add  8147  apreap  8161  lemul1  8167  reapmul1lem  8168  reapmul1  8169  reapadd1  8170  remulext1  8173  remulext2  8174  apadd2  8183  mulext2  8187  mulap0r  8189  leltap  8198  ltap  8205  apsub1  8214  recexaplem2  8218  mulcanap  8231  mulcanap2  8232  divvalap  8238  divmulap  8239  divcanap1  8245  diveqap0  8246  divap0b  8247  divrecap  8252  divassap  8254  div23ap  8255  divdirap  8261  divcanap3  8262  div11ap  8264  diveqap1  8269  divmuldivap  8276  divcanap5  8278  redivclap  8295  div2negap  8299  apmul1  8352  apmul2  8353  div2subap  8399  ltdiv1  8426  ledivmul  8435  lemuldiv  8439  lt2msq1  8443  ltdiv23  8450  squeeze0  8462  zaddcllemneg  8887  eluzsub  9147  nn01to3  9201  rpgecl  9261  addlelt  9338  xleadd1  9441  xltadd1  9442  lbioog  9479  ubioc1  9495  ubicc2  9551  icoshftf1o  9557  fzen  9606  ubmelfzo  9760  ssfzo12  9784  ubmelm1fzo  9786  fzosplitprm1  9794  rebtwn2zlemshrink  9814  qbtwnre  9817  flqwordi  9844  flqword2  9845  flltdivnn0lt  9860  modqcl  9882  mulqmod0  9886  modqmulnn  9898  modqabs2  9914  modqmuladdnn0  9924  qnegmod  9925  addmodid  9928  modqm1p1mod0  9931  modifeq2int  9942  modqdi  9948  modqeqmodmin  9950  modfzo0difsn  9951  frec2uzf1od  9962  exp3val  10072  expnegap0  10078  expgt1  10108  exprecap  10111  expmulzap  10116  leexp2a  10123  expubnd  10127  mulbinom2  10185  bernneq2  10190  expnbnd  10192  fihashss  10339  fihashssdif  10341  fimaxq  10350  shftuz  10366  shftfibg  10369  cjdivap  10458  resqrtcl  10577  absdivap  10618  abssubne0  10639  maxleast  10761  lemininf  10780  ltmininf  10781  xrmaxltsup  10801  xrmaxaddlem  10803  xrmaxadd  10804  xrmineqinf  10812  xrltmininf  10813  xrminltinf  10815  xrminadd  10818  climuni  10836  reccn2ap  10856  isumz  10932  geoisum1c  11063  efltim  11137  dvdsval2  11226  dvdscmulr  11252  dvdsmulcr  11253  modmulconst  11255  dvdsadd2b  11270  dvdsexp  11289  mulmoddvds  11291  divalglemeuneg  11350  gcdaddm  11402  dvdsgcdb  11429  mulgcd  11432  gcddiv  11435  lcmdvdsb  11493  mulgcddvds  11503  qredeq  11505  divgcdcoprm0  11510  cncongr1  11512  euclemma  11552  rpexp  11559  rpexp12i  11561  fvsetsid  11677  ressid2  11702  ressval2  11703  rngplusgg  11760  2basgeng  11934  iuncld  11967  ntrss  11971  restco  12026  restabs  12027  cnprcl2k  12057  lmconst  12067  cnrest2  12087  psmetsym  12115  psmetge0  12117  xmetge0  12151  xmetsym  12154  blvalps  12174  blval  12175  xblcntrps  12199  xblcntr  12200  xmssym  12255  blsscls2  12279  bdxmet  12287  findset  12548