Theorem simp2lr 1242

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

Assertion

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

Proof of Theorem simp2lr

Step	Hyp	Ref	Expression
1		simplr 768	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant2 1135	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 206  df-an 398  df-3an 1090

This theorem is referenced by:  fpr3g  8270  tfrlem5  8380  omeu  8585  expmordi  14132  4sqlem18  16895  vdwlem10  16923  mvrf1  21545  mdetuni0  22123  mdetmul  22125  tsmsxp  23659  ax5seglem3  28189  btwnconn1lem1  35059  btwnconn1lem3  35061  btwnconn1lem4  35062  btwnconn1lem5  35063  btwnconn1lem6  35064  btwnconn1lem7  35065  linethru  35125  lshpkrlem6  37985  athgt  38327  2llnjN  38438  dalaw  38757  cdlemb2  38912  4atexlemex6  38945  cdleme01N  39092  cdleme0ex2N  39095  cdleme7aa  39113  cdleme7e  39118  cdlemg33c0  39573  dihmeetlem3N  40176  pellex  41573