Theorem simp3rr 1260

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

Assertion

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

Proof of Theorem simp3rr

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  poxp3  8125  omeu  8549  ntrivcvgmul  15915  tsmsxp  24195  tgqioo  24840  ovolunlem2  25540  plyadd  26257  plymul  26258  coeeu  26265  nosupbnd1lem2  27750  noinfbnd1lem2  27765  tghilberti2  28784  cvmlift2lem10  35626  btwnconn1lem1  36401  lplnexllnN  40152  2llnjN  40155  4atlem12b  40199  lplncvrlvol2  40203  lncmp  40371  cdlema2N  40380  cdleme11a  40848  cdleme24  40940  cdleme28  40961  cdlemefr29bpre0N  40994  cdlemefr29clN  40995  cdlemefr32fvaN  40997  cdlemefr32fva1  40998  cdlemefs29bpre0N  41004  cdlemefs29bpre1N  41005  cdlemefs29cpre1N  41006  cdlemefs29clN  41007  cdlemefs32fvaN  41010  cdlemefs32fva1  41011  cdleme36m  41049  cdleme17d3  41084  cdlemg36  41302  cdlemj3  41411  cdlemkid1  41510  cdlemk19ylem  41518  cdlemk19xlem  41530  dihlsscpre  41822  dihord4  41846  dihmeetlem1N  41878  dihatlat  41922  jm2.27  43549