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  8132  omeu  8552  ntrivcvgmul  15875  tsmsxp  24049  tgqioo  24695  ovolunlem2  25406  plyadd  26129  plymul  26130  coeeu  26137  nosupbnd1lem2  27628  noinfbnd1lem2  27643  tghilberti2  28572  cvmlift2lem10  35306  btwnconn1lem1  36082  lplnexllnN  39565  2llnjN  39568  4atlem12b  39612  lplncvrlvol2  39616  lncmp  39784  cdlema2N  39793  cdleme11a  40261  cdleme24  40353  cdleme28  40374  cdlemefr29bpre0N  40407  cdlemefr29clN  40408  cdlemefr32fvaN  40410  cdlemefr32fva1  40411  cdlemefs29bpre0N  40417  cdlemefs29bpre1N  40418  cdlemefs29cpre1N  40419  cdlemefs29clN  40420  cdlemefs32fvaN  40423  cdlemefs32fva1  40424  cdleme36m  40462  cdleme17d3  40497  cdlemg36  40715  cdlemj3  40824  cdlemkid1  40923  cdlemk19ylem  40931  cdlemk19xlem  40943  dihlsscpre  41235  dihord4  41259  dihmeetlem1N  41291  dihatlat  41335  jm2.27  43004