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  8092  omeu  8512  ntrivcvgmul  15825  tsmsxp  24099  tgqioo  24744  ovolunlem2  25455  plyadd  26178  plymul  26179  coeeu  26186  nosupbnd1lem2  27677  noinfbnd1lem2  27692  tghilberti2  28710  cvmlift2lem10  35506  btwnconn1lem1  36281  lplnexllnN  39820  2llnjN  39823  4atlem12b  39867  lplncvrlvol2  39871  lncmp  40039  cdlema2N  40048  cdleme11a  40516  cdleme24  40608  cdleme28  40629  cdlemefr29bpre0N  40662  cdlemefr29clN  40663  cdlemefr32fvaN  40665  cdlemefr32fva1  40666  cdlemefs29bpre0N  40672  cdlemefs29bpre1N  40673  cdlemefs29cpre1N  40674  cdlemefs29clN  40675  cdlemefs32fvaN  40678  cdlemefs32fva1  40679  cdleme36m  40717  cdleme17d3  40752  cdlemg36  40970  cdlemj3  41079  cdlemkid1  41178  cdlemk19ylem  41186  cdlemk19xlem  41198  dihlsscpre  41490  dihord4  41514  dihmeetlem1N  41546  dihatlat  41590  jm2.27  43246