Theorem simp2lr 1258

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

Assertion

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

Proof of Theorem simp2lr

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  fpr3g  8270  tfrlem5  8354  omeu  8558  expmordi  14194  4sqlem18  17012  vdwlem10  17040  mvrf1  22095  mdetuni0  22739  mdetmul  22741  tsmsxp  24273  ax5seglem3  29190  btwnconn1lem1  36450  btwnconn1lem3  36452  btwnconn1lem4  36453  btwnconn1lem5  36454  btwnconn1lem6  36455  btwnconn1lem7  36456  linethru  36516  lshpkrlem6  39751  athgt  40092  2llnjN  40203  dalaw  40522  cdlemb2  40677  4atexlemex6  40710  cdleme01N  40857  cdleme0ex2N  40860  cdleme7aa  40878  cdleme7e  40883  cdlemg33c0  41338  dihmeetlem3N  41941  pellex  43424