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 399   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  omeu  8245  ntrivcvgmul  15353  tsmsxp  22909  tgqioo  23555  ovolunlem2  24253  plyadd  24969  plymul  24970  coeeu  24977  tghilberti2  26587  cvmlift2lem10  32848  nosupbnd1lem2  33558  noinfbnd1lem2  33573  btwnconn1lem1  34035  lplnexllnN  37224  2llnjN  37227  4atlem12b  37271  lplncvrlvol2  37275  lncmp  37443  cdlema2N  37452  cdleme11a  37920  cdleme24  38012  cdleme28  38033  cdlemefr29bpre0N  38066  cdlemefr29clN  38067  cdlemefr32fvaN  38069  cdlemefr32fva1  38070  cdlemefs29bpre0N  38076  cdlemefs29bpre1N  38077  cdlemefs29cpre1N  38078  cdlemefs29clN  38079  cdlemefs32fvaN  38082  cdlemefs32fva1  38083  cdleme36m  38121  cdleme17d3  38156  cdlemg36  38374  cdlemj3  38483  cdlemkid1  38582  cdlemk19ylem  38590  cdlemk19xlem  38602  dihlsscpre  38894  dihord4  38918  dihmeetlem1N  38950  dihatlat  38994  jm2.27  40425