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  8149  omeu  8597  ntrivcvgmul  15918  tsmsxp  24093  tgqioo  24739  ovolunlem2  25451  plyadd  26174  plymul  26175  coeeu  26182  nosupbnd1lem2  27673  noinfbnd1lem2  27688  tghilberti2  28617  cvmlift2lem10  35334  btwnconn1lem1  36105  lplnexllnN  39583  2llnjN  39586  4atlem12b  39630  lplncvrlvol2  39634  lncmp  39802  cdlema2N  39811  cdleme11a  40279  cdleme24  40371  cdleme28  40392  cdlemefr29bpre0N  40425  cdlemefr29clN  40426  cdlemefr32fvaN  40428  cdlemefr32fva1  40429  cdlemefs29bpre0N  40435  cdlemefs29bpre1N  40436  cdlemefs29cpre1N  40437  cdlemefs29clN  40438  cdlemefs32fvaN  40441  cdlemefs32fva1  40442  cdleme36m  40480  cdleme17d3  40515  cdlemg36  40733  cdlemj3  40842  cdlemkid1  40941  cdlemk19ylem  40949  cdlemk19xlem  40961  dihlsscpre  41253  dihord4  41277  dihmeetlem1N  41309  dihatlat  41353  jm2.27  43032