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  8237  tfrlem5  8321  omeu  8522  expmordi  14102  4sqlem18  16902  vdwlem10  16930  mvrf1  21953  mdetuni0  22577  mdetmul  22579  tsmsxp  24111  ax5seglem3  29016  btwnconn1lem1  36300  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem5  36304  btwnconn1lem6  36305  btwnconn1lem7  36306  linethru  36366  lshpkrlem6  39485  athgt  39826  2llnjN  39937  dalaw  40256  cdlemb2  40411  4atexlemex6  40444  cdleme01N  40591  cdleme0ex2N  40594  cdleme7aa  40612  cdleme7e  40617  cdlemg33c0  41072  dihmeetlem3N  41675  pellex  43186