Theorem simp2lr 1243

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

Assertion

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

Proof of Theorem simp2lr

Step	Hyp	Ref	Expression
1		simplr 769	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant2 1135	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:  fpr3g  8226  tfrlem5  8310  omeu  8511  expmordi  14091  4sqlem18  16891  vdwlem10  16919  mvrf1  21942  mdetuni0  22564  mdetmul  22566  tsmsxp  24098  ax5seglem3  28988  btwnconn1lem1  36275  btwnconn1lem3  36277  btwnconn1lem4  36278  btwnconn1lem5  36279  btwnconn1lem6  36280  btwnconn1lem7  36281  linethru  36341  lshpkrlem6  39552  athgt  39893  2llnjN  40004  dalaw  40323  cdlemb2  40478  4atexlemex6  40511  cdleme01N  40658  cdleme0ex2N  40661  cdleme7aa  40679  cdleme7e  40684  cdlemg33c0  41139  dihmeetlem3N  41742  pellex  43266