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  8235  tfrlem5  8319  omeu  8520  expmordi  14129  4sqlem18  16933  vdwlem10  16961  mvrf1  21964  mdetuni0  22586  mdetmul  22588  tsmsxp  24120  ax5seglem3  29000  btwnconn1lem1  36269  btwnconn1lem3  36271  btwnconn1lem4  36272  btwnconn1lem5  36273  btwnconn1lem6  36274  btwnconn1lem7  36275  linethru  36335  lshpkrlem6  39561  athgt  39902  2llnjN  40013  dalaw  40332  cdlemb2  40487  4atexlemex6  40520  cdleme01N  40667  cdleme0ex2N  40670  cdleme7aa  40688  cdleme7e  40693  cdlemg33c0  41148  dihmeetlem3N  41751  pellex  43263