Theorem simp2 942

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

Syntax hints:   → wi 4   ∧ w3a 922

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

This theorem depends on definitions:  df-bi 115  df-3an 924

This theorem is referenced by:  simpl2  945  simpr2  948  simp2i  951  simp2d  954  simp12  972  simp22  975  simp32  978  syld3an3  1217  3ianorr  1243  stoic4b  1365  nlim0  4195  tfisi  4375  sotri2  4796  sotri3  4797  feq123  5118  sefvex  5289  fvmptt  5357  fnfvima  5490  cocan1  5527  cocan2  5528  ovexg  5640  ovmpt2x  5730  ovmpt2ga  5731  caovimo  5795  tfr1onlembxssdm  6062  tfr1onlembfn  6063  tfrcllembxssdm  6075  tfrcllembfn  6076  freccllem  6121  frecfcllem  6123  frecsuclem  6125  frecrdg  6127  mapxpen  6516  dif1en  6547  diffifi  6562  unsnfidcex  6582  unfidisj  6584  undifdc  6586  resfnfinfinss  6599  funrnfi  6601  sbthlemi9  6618  mulcanenq  6888  ltanqg  6903  mulcanenq0ec  6948  addnnnq0  6952  distrprg  7091  aptipr  7144  addsrpr  7235  mulsrpr  7236  mulasssrg  7248  axmulass  7352  axpre-ltadd  7365  subadd2  7630  nppcan  7648  nppcan3  7650  subsub2  7654  subsub4  7659  npncan3  7664  pnpcan  7665  pnncan  7667  subcan  7681  ltadd1  7851  leadd1  7852  leadd2  7853  ltsubadd  7854  ltsubadd2  7855  lesubadd  7856  lesubadd2  7857  ltaddsub  7858  leaddsub  7860  lesub1  7878  lesub2  7879  ltsub1  7880  ltsub2  7881  gt0add  7991  apreap  8005  lemul1  8011  reapmul1lem  8012  reapmul1  8013  reapadd1  8014  remulext1  8017  remulext2  8018  apadd2  8027  mulext2  8031  mulap0r  8033  leltap  8042  ltap  8049  recexaplem2  8060  mulcanap  8073  mulcanap2  8074  divvalap  8080  divmulap  8081  divcanap1  8087  diveqap0  8088  divap0b  8089  divrecap  8094  divassap  8096  div23ap  8097  divdirap  8103  divcanap3  8104  div11ap  8106  diveqap1  8111  divmuldivap  8118  divcanap5  8120  redivclap  8137  div2negap  8141  apmul1  8194  ltdiv1  8264  ledivmul  8273  lemuldiv  8277  lt2msq1  8281  ltdiv23  8288  squeeze0  8300  zaddcllemneg  8722  eluzsub  8980  nn01to3  9034  rpgecl  9094  addlelt  9171  lbioog  9263  ubioc1  9279  ubicc2  9334  icoshftf1o  9340  fzen  9389  ubmelfzo  9539  ssfzo12  9563  ubmelm1fzo  9565  fzosplitprm1  9573  rebtwn2zlemshrink  9593  qbtwnre  9596  flqwordi  9623  flqword2  9624  flltdivnn0lt  9639  modqcl  9661  mulqmod0  9665  modqmulnn  9677  modqabs2  9693  modqmuladdnn0  9703  qnegmod  9704  addmodid  9707  modqm1p1mod0  9710  modifeq2int  9721  modqdi  9727  modqeqmodmin  9729  modfzo0difsn  9730  frec2uzf1od  9741  expnegap0  9862  expgt1  9892  exprecap  9895  expmulzap  9900  leexp2a  9907  expubnd  9911  mulbinom2  9967  bernneq2  9972  expnbnd  9974  fihashss  10121  fihashssdif  10123  fimaxq  10132  shftuz  10148  shftfibg  10151  cjdivap  10239  resqrtcl  10358  absdivap  10399  abssubne0  10420  maxleast  10542  lemininf  10559  ltmininf  10560  climuni  10576  isumz  10669  dvdsval2  10681  dvdscmulr  10707  dvdsmulcr  10708  modmulconst  10710  dvdsadd2b  10725  dvdsexp  10744  mulmoddvds  10746  divalglemeuneg  10805  gcdaddm  10857  dvdsgcdb  10884  mulgcd  10887  gcddiv  10890  lcmdvdsb  10948  mulgcddvds  10958  qredeq  10960  divgcdcoprm0  10965  cncongr1  10967  euclemma  11007  rpexp  11014  rpexp12i  11016  findset  11285