Theorem simp3rr 1248

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp3rr	⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓)

Proof of Theorem simp3rr

Step	Hyp	Ref	Expression
1		simprr 772	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant3 1135	1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp3  8086  omeu  8506  ntrivcvgmul  15811  tsmsxp  24071  tgqioo  24716  ovolunlem2  25427  plyadd  26150  plymul  26151  coeeu  26158  nosupbnd1lem2  27649  noinfbnd1lem2  27664  tghilberti2  28617  cvmlift2lem10  35377  btwnconn1lem1  36152  lplnexllnN  39683  2llnjN  39686  4atlem12b  39730  lplncvrlvol2  39734  lncmp  39902  cdlema2N  39911  cdleme11a  40379  cdleme24  40471  cdleme28  40492  cdlemefr29bpre0N  40525  cdlemefr29clN  40526  cdlemefr32fvaN  40528  cdlemefr32fva1  40529  cdlemefs29bpre0N  40535  cdlemefs29bpre1N  40536  cdlemefs29cpre1N  40537  cdlemefs29clN  40538  cdlemefs32fvaN  40541  cdlemefs32fva1  40542  cdleme36m  40580  cdleme17d3  40615  cdlemg36  40833  cdlemj3  40942  cdlemkid1  41041  cdlemk19ylem  41049  cdlemk19xlem  41061  dihlsscpre  41353  dihord4  41377  dihmeetlem1N  41409  dihatlat  41453  jm2.27  43125