Theorem simp3rr 1264

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

Assertion

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

Proof of Theorem simp3rr

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  poxp3  8134  omeu  8558  ntrivcvgmul  15946  tsmsxp  24273  tgqioo  24918  ovolunlem2  25618  plyadd  26335  plymul  26336  coeeu  26343  nosupbnd1lem2  27831  noinfbnd1lem2  27846  tghilberti2  28865  cvmlift2lem10  35675  btwnconn1lem1  36450  lplnexllnN  40200  2llnjN  40203  4atlem12b  40247  lplncvrlvol2  40251  lncmp  40419  cdlema2N  40428  cdleme11a  40896  cdleme24  40988  cdleme28  41009  cdlemefr29bpre0N  41042  cdlemefr29clN  41043  cdlemefr32fvaN  41045  cdlemefr32fva1  41046  cdlemefs29bpre0N  41052  cdlemefs29bpre1N  41053  cdlemefs29cpre1N  41054  cdlemefs29clN  41055  cdlemefs32fvaN  41058  cdlemefs32fva1  41059  cdleme36m  41097  cdleme17d3  41132  cdlemg36  41350  cdlemj3  41459  cdlemkid1  41558  cdlemk19ylem  41566  cdlemk19xlem  41578  dihlsscpre  41870  dihord4  41894  dihmeetlem1N  41926  dihatlat  41970  jm2.27  43597