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 1134	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  fpr3g  8264  tfrlem5  8348  omeu  8549  expmordi  14132  4sqlem18  16933  vdwlem10  16961  mvrf1  21895  mdetuni0  22508  mdetmul  22510  tsmsxp  24042  ax5seglem3  28858  btwnconn1lem1  36075  btwnconn1lem3  36077  btwnconn1lem4  36078  btwnconn1lem5  36079  btwnconn1lem6  36080  btwnconn1lem7  36081  linethru  36141  lshpkrlem6  39108  athgt  39450  2llnjN  39561  dalaw  39880  cdlemb2  40035  4atexlemex6  40068  cdleme01N  40215  cdleme0ex2N  40218  cdleme7aa  40236  cdleme7e  40241  cdlemg33c0  40696  dihmeetlem3N  41299  pellex  42823