Theorem simp2 983

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

Syntax hints:   → wi 4   ∧ w3a 963

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

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

This theorem is referenced by:  simpl2  986  simpr2  989  simp2i  992  simp2d  995  simp12  1013  simp22  1016  simp32  1019  syld3an3  1262  3ianorr  1288  stoic4b  1410  nlim0  4324  tfisi  4509  sotri2  4944  sotri3  4945  feq123  5272  sefvex  5450  fvmptt  5520  fnfvima  5660  cocan1  5696  cocan2  5697  ovexg  5813  ovmpox  5907  ovmpoga  5908  caovimo  5972  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfrcllembxssdm  6261  tfrcllembfn  6262  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecrdg  6313  mapxpen  6750  dif1en  6781  diffifi  6796  unsnfidcex  6816  unfidisj  6818  undifdc  6820  resfnfinfinss  6836  funrnfi  6838  sbthlemi9  6861  elfir  6869  difinfsn  6993  ctssdc  7006  djuassen  7090  xpdjuen  7091  mulcanenq  7217  ltanqg  7232  mulcanenq0ec  7277  addnnnq0  7281  distrprg  7420  aptipr  7473  addsrpr  7577  mulsrpr  7578  mulasssrg  7590  ltpsrprg  7635  axmulass  7705  axpre-ltadd  7718  subadd2  7990  nppcan  8008  nppcan3  8010  subsub2  8014  subsub4  8019  npncan3  8024  pnpcan  8025  pnncan  8027  subcan  8041  ltadd1  8215  leadd1  8216  leadd2  8217  ltsubadd  8218  ltsubadd2  8219  lesubadd  8220  lesubadd2  8221  ltaddsub  8222  leaddsub  8224  lesub1  8242  lesub2  8243  ltsub1  8244  ltsub2  8245  gt0add  8359  apreap  8373  lemul1  8379  reapmul1lem  8380  reapmul1  8381  reapadd1  8382  remulext1  8385  remulext2  8386  apadd2  8395  mulext2  8399  mulap0r  8401  leltap  8411  ltap  8419  apsub1  8428  recexaplem2  8437  mulcanap  8450  mulcanap2  8451  divvalap  8458  divmulap  8459  divcanap1  8465  diveqap0  8466  divap0b  8467  divrecap  8472  divassap  8474  div23ap  8475  divdirap  8481  divcanap3  8482  div11ap  8484  diveqap1  8489  divmuldivap  8496  divcanap5  8498  redivclap  8515  div2negap  8519  apmul1  8572  apmul2  8573  div2subap  8620  ltdiv1  8650  ledivmul  8659  lemuldiv  8663  lt2msq1  8667  ltdiv23  8674  squeeze0  8686  zaddcllemneg  9117  eluzsub  9379  nn01to3  9436  rpgecl  9499  addlelt  9585  xleadd1  9688  xltadd1  9689  lbioog  9726  ubioc1  9742  ubicc2  9798  icoshftf1o  9804  fzen  9854  ubmelfzo  10008  ssfzo12  10032  ubmelm1fzo  10034  fzosplitprm1  10042  rebtwn2zlemshrink  10062  qbtwnre  10065  flqwordi  10092  flqword2  10093  flltdivnn0lt  10108  modqcl  10130  mulqmod0  10134  modqmulnn  10146  modqabs2  10162  modqmuladdnn0  10172  qnegmod  10173  addmodid  10176  modqm1p1mod0  10179  modifeq2int  10190  modqdi  10196  modqeqmodmin  10198  modfzo0difsn  10199  frec2uzf1od  10210  exp3val  10326  expnegap0  10332  expgt1  10362  exprecap  10365  expmulzap  10370  leexp2a  10377  expubnd  10381  mulbinom2  10439  bernneq2  10444  expnbnd  10446  fihashss  10594  fihashssdif  10596  fimaxq  10605  shftuz  10621  shftfibg  10624  cjdivap  10713  resqrtcl  10833  absdivap  10874  abssubne0  10895  maxleast  11017  lemininf  11037  ltmininf  11038  xrmaxltsup  11059  xrmaxaddlem  11061  xrmaxadd  11062  xrmineqinf  11070  xrltmininf  11071  xrminltinf  11073  xrminadd  11076  climuni  11094  reccn2ap  11114  isumz  11190  geoisum1c  11321  efltim  11441  dvdsval2  11532  dvdscmulr  11558  dvdsmulcr  11559  modmulconst  11561  dvdsadd2b  11576  dvdsexp  11595  mulmoddvds  11597  divalglemeuneg  11656  gcdaddm  11708  dvdsgcdb  11737  mulgcd  11740  gcddiv  11743  lcmdvdsb  11801  mulgcddvds  11811  qredeq  11813  divgcdcoprm0  11818  cncongr1  11820  euclemma  11860  rpexp  11867  rpexp12i  11869  ctinf  11979  fvsetsid  12032  ressid2  12057  ressval2  12058  rngplusgg  12115  2basgeng  12290  iuncld  12323  ntrss  12327  restco  12382  restabs  12383  cnprcl2k  12414  lmconst  12424  cnrest2  12444  cnmpt2t  12501  psmetsym  12537  psmetge0  12539  xmetge0  12573  xmetsym  12576  blvalps  12596  blval  12597  xblcntrps  12621  xblcntr  12622  xmssym  12677  blsscls2  12701  bdxmet  12709  txmetcnp  12726  dvfvalap  12858  dvid  12870  dvcnp2cntop  12871  rpcxpadd  13034  rpcxpsub  13037  rpmulcxp  13038  rpdivcxp  13040  cxpmul  13041  rpcxple2  13046  rpcxplt2  13047  rplogbval  13070  rplogbcl  13071  rplogbreexp  13078  relogbexpap  13083  logbleb  13086  logblt  13087  rplogbcxp  13088  rpcxplogb  13089  relogbcxpbap  13090  findset  13314