Theorem simp2 904

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 900	. 2 ⊢ ((φ ∧ ψ ∧ χ) → (φ ∧ ψ))
2	1	simprd 107	1 ⊢ ((φ ∧ ψ ∧ χ) → ψ)

Syntax hints:   → wi 4   ∧ w3a 884

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

This theorem depends on definitions:  df-bi 110  df-3an 886

This theorem is referenced by:  simpl2  907  simpr2  910  simp2i  913  simp2d  916  simp12  934  simp22  937  simp32  940  syld3an3  1179  3ianorr  1203  stoic4b  1319  nlim0  4097  tfisi  4253  sotri2  4665  sotri3  4666  feq123  4981  sefvex  5139  fvmptt  5205  fnfvima  5336  cocan1  5370  cocan2  5371  ovmpt2x  5571  ovmpt2ga  5572  caovimo  5636  frecsuclem3  5929  mulcanenq  6369  ltanqg  6384  mulcanenq0ec  6428  addnnnq0  6432  distrprg  6564  aptipr  6613  addsrpr  6673  mulsrpr  6674  mulasssrg  6686  axmulass  6757  axpre-ltadd  6770  subadd2  7012  nppcan  7029  nppcan3  7031  subsub2  7035  subsub4  7040  npncan3  7045  pnpcan  7046  pnncan  7048  subcan  7062  ltadd1  7219  leadd1  7220  leadd2  7221  ltsubadd  7222  ltsubadd2  7223  lesubadd  7224  lesubadd2  7225  ltaddsub  7226  leaddsub  7228  lesub1  7246  lesub2  7247  ltsub1  7248  ltsub2  7249  gt0add  7357  apreap  7371  lemul1  7377  reapmul1lem  7378  reapmul1  7379  reapadd1  7380  remulext1  7383  remulext2  7384  apadd2  7393  mulext2  7397  mulap0r  7399  recexaplem2  7415  mulcanap  7428  mulcanap2  7429  divvalap  7435  divmulap  7436  divcanap1  7442  diveqap0  7443  divap0b  7444  divrecap  7449  divassap  7451  div23ap  7452  divdirap  7456  divcanap3  7457  div11ap  7459  diveqap1  7464  divmuldivap  7470  divcanap5  7472  redivclap  7489  div2negap  7493  apmul1  7546  ltdiv1  7615  ledivmul  7624  lemuldiv  7628  lt2msq1  7632  ltdiv23  7639  squeeze0  7651  zaddcllemneg  8060  eluzsub  8278  nn01to3  8328  rpgecl  8386  lbioog  8552  ubioc1  8568  ubicc2  8623  icoshftf1o  8629  fzen  8677  ubmelfzo  8826  ssfzo12  8850  ubmelm1fzo  8852  fzosplitprm1  8860  frec2uzf1od  8873  expnegap0  8917  expgt1  8947  exprecap  8950  expmulzap  8955  leexp2a  8961  expubnd  8965  bernneq2  9023  expnbnd  9025  cjdivap  9137  findset  9405