Theorem simp2lr 1238

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

Assertion

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

Proof of Theorem simp2lr

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  fpr3g  8289  tfrlem5  8399  omeu  8604  expmordi  14163  4sqlem18  16930  vdwlem10  16958  mvrf1  21935  mdetuni0  22553  mdetmul  22555  tsmsxp  24089  ax5seglem3  28798  btwnconn1lem1  35753  btwnconn1lem3  35755  btwnconn1lem4  35756  btwnconn1lem5  35757  btwnconn1lem6  35758  btwnconn1lem7  35759  linethru  35819  lshpkrlem6  38656  athgt  38998  2llnjN  39109  dalaw  39428  cdlemb2  39583  4atexlemex6  39616  cdleme01N  39763  cdleme0ex2N  39766  cdleme7aa  39784  cdleme7e  39789  cdlemg33c0  40244  dihmeetlem3N  40847  pellex  42320