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 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  8175  omeu  8623  ntrivcvgmul  15938  tsmsxp  24163  tgqioo  24821  ovolunlem2  25533  plyadd  26256  plymul  26257  coeeu  26264  nosupbnd1lem2  27754  noinfbnd1lem2  27769  tghilberti2  28646  cvmlift2lem10  35317  btwnconn1lem1  36088  lplnexllnN  39566  2llnjN  39569  4atlem12b  39613  lplncvrlvol2  39617  lncmp  39785  cdlema2N  39794  cdleme11a  40262  cdleme24  40354  cdleme28  40375  cdlemefr29bpre0N  40408  cdlemefr29clN  40409  cdlemefr32fvaN  40411  cdlemefr32fva1  40412  cdlemefs29bpre0N  40418  cdlemefs29bpre1N  40419  cdlemefs29cpre1N  40420  cdlemefs29clN  40421  cdlemefs32fvaN  40424  cdlemefs32fva1  40425  cdleme36m  40463  cdleme17d3  40498  cdlemg36  40716  cdlemj3  40825  cdlemkid1  40924  cdlemk19ylem  40932  cdlemk19xlem  40944  dihlsscpre  41236  dihord4  41260  dihmeetlem1N  41292  dihatlat  41336  jm2.27  43020