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  8306  tfrlem5  8390  omeu  8596  expmordi  14313  4sqlem18  17145  vdwlem10  17173  mvrf1  22298  mdetuni0  22941  mdetmul  22943  tsmsxp  24479  ax5seglem3  29514  btwnconn1lem1  36944  btwnconn1lem3  36946  btwnconn1lem4  36947  btwnconn1lem5  36948  btwnconn1lem6  36949  btwnconn1lem7  36950  linethru  37010  lshpkrlem6  40265  athgt  40606  2llnjN  40717  dalaw  41036  cdlemb2  41191  4atexlemex6  41224  cdleme01N  41371  cdleme0ex2N  41374  cdleme7aa  41392  cdleme7e  41397  cdlemg33c0  41852  dihmeetlem3N  42455  pellex  43935