Theorem simp3rr 1247

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

Assertion

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

Proof of Theorem simp3rr

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  poxp3  8135  omeu  8584  ntrivcvgmul  15847  tsmsxp  23658  tgqioo  24315  ovolunlem2  25014  plyadd  25730  plymul  25731  coeeu  25738  nosupbnd1lem2  27209  noinfbnd1lem2  27224  tghilberti2  27886  cvmlift2lem10  34298  btwnconn1lem1  35054  lplnexllnN  38430  2llnjN  38433  4atlem12b  38477  lplncvrlvol2  38481  lncmp  38649  cdlema2N  38658  cdleme11a  39126  cdleme24  39218  cdleme28  39239  cdlemefr29bpre0N  39272  cdlemefr29clN  39273  cdlemefr32fvaN  39275  cdlemefr32fva1  39276  cdlemefs29bpre0N  39282  cdlemefs29bpre1N  39283  cdlemefs29cpre1N  39284  cdlemefs29clN  39285  cdlemefs32fvaN  39288  cdlemefs32fva1  39289  cdleme36m  39327  cdleme17d3  39362  cdlemg36  39580  cdlemj3  39689  cdlemkid1  39788  cdlemk19ylem  39796  cdlemk19xlem  39808  dihlsscpre  40100  dihord4  40124  dihmeetlem1N  40156  dihatlat  40200  jm2.27  41737