Theorem simp2lr 1254

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

Assertion

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

Proof of Theorem simp2lr

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  fpr3g  8261  tfrlem5  8345  omeu  8549  expmordi  14177  4sqlem18  16981  vdwlem10  17009  mvrf1  22017  mdetuni0  22661  mdetmul  22663  tsmsxp  24195  ax5seglem3  29078  btwnconn1lem1  36401  btwnconn1lem3  36403  btwnconn1lem4  36404  btwnconn1lem5  36405  btwnconn1lem6  36406  btwnconn1lem7  36407  linethru  36467  lshpkrlem6  39703  athgt  40044  2llnjN  40155  dalaw  40474  cdlemb2  40629  4atexlemex6  40662  cdleme01N  40809  cdleme0ex2N  40812  cdleme7aa  40830  cdleme7e  40835  cdlemg33c0  41290  dihmeetlem3N  41893  pellex  43376