Theorem simp2lr 1241

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

Assertion

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

Proof of Theorem simp2lr

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

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

This theorem is referenced by:  fpr3g  8269  tfrlem5  8379  omeu  8584  expmordi  14131  4sqlem18  16894  vdwlem10  16922  mvrf1  21544  mdetuni0  22122  mdetmul  22124  tsmsxp  23658  ax5seglem3  28186  btwnconn1lem1  35054  btwnconn1lem3  35056  btwnconn1lem4  35057  btwnconn1lem5  35058  btwnconn1lem6  35059  btwnconn1lem7  35060  linethru  35120  lshpkrlem6  37980  athgt  38322  2llnjN  38433  dalaw  38752  cdlemb2  38907  4atexlemex6  38940  cdleme01N  39087  cdleme0ex2N  39090  cdleme7aa  39108  cdleme7e  39113  cdlemg33c0  39568  dihmeetlem3N  40171  pellex  41563