Theorem simp2lr 1260

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

Assertion

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

Proof of Theorem simp2lr

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  fpr3g  8287  tfrlem5  8371  omeu  8577  expmordi  14290  4sqlem18  17120  vdwlem10  17148  mvrf1  22273  mdetuni0  22916  mdetmul  22918  tsmsxp  24454  ax5seglem3  29491  btwnconn1lem1  36822  btwnconn1lem3  36824  btwnconn1lem4  36825  btwnconn1lem5  36826  btwnconn1lem6  36827  btwnconn1lem7  36828  linethru  36888  lshpkrlem6  40140  athgt  40481  2llnjN  40592  dalaw  40911  cdlemb2  41066  4atexlemex6  41099  cdleme01N  41246  cdleme0ex2N  41249  cdleme7aa  41267  cdleme7e  41272  cdlemg33c0  41727  dihmeetlem3N  42330  pellex  43795