Theorem simp3rr 1249

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

Assertion

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

Proof of Theorem simp3rr

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  poxp3  8102  omeu  8522  ntrivcvgmul  15837  tsmsxp  24111  tgqioo  24756  ovolunlem2  25467  plyadd  26190  plymul  26191  coeeu  26198  nosupbnd1lem2  27689  noinfbnd1lem2  27704  tghilberti2  28722  cvmlift2lem10  35525  btwnconn1lem1  36300  lplnexllnN  39934  2llnjN  39937  4atlem12b  39981  lplncvrlvol2  39985  lncmp  40153  cdlema2N  40162  cdleme11a  40630  cdleme24  40722  cdleme28  40743  cdlemefr29bpre0N  40776  cdlemefr29clN  40777  cdlemefr32fvaN  40779  cdlemefr32fva1  40780  cdlemefs29bpre0N  40786  cdlemefs29bpre1N  40787  cdlemefs29cpre1N  40788  cdlemefs29clN  40789  cdlemefs32fvaN  40792  cdlemefs32fva1  40793  cdleme36m  40831  cdleme17d3  40866  cdlemg36  41084  cdlemj3  41193  cdlemkid1  41292  cdlemk19ylem  41300  cdlemk19xlem  41312  dihlsscpre  41604  dihord4  41628  dihmeetlem1N  41660  dihatlat  41704  jm2.27  43359