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  8334  tfrlem5  8418  omeu  8624  expmordi  14340  4sqlem18  17172  vdwlem10  17200  mvrf1  22326  mdetuni0  22969  mdetmul  22971  tsmsxp  24507  ax5seglem3  29542  btwnconn1lem1  37043  btwnconn1lem3  37045  btwnconn1lem4  37046  btwnconn1lem5  37047  btwnconn1lem6  37048  btwnconn1lem7  37049  linethru  37109  lshpkrlem6  40375  athgt  40716  2llnjN  40827  dalaw  41146  cdlemb2  41301  4atexlemex6  41334  cdleme01N  41481  cdleme0ex2N  41484  cdleme7aa  41502  cdleme7e  41507  cdlemg33c0  41962  dihmeetlem3N  42565  pellex  44046