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  8304  tfrlem5  8388  omeu  8594  expmordi  14311  4sqlem18  17141  vdwlem10  17169  mvrf1  22294  mdetuni0  22937  mdetmul  22939  tsmsxp  24475  ax5seglem3  29510  btwnconn1lem1  36853  btwnconn1lem3  36855  btwnconn1lem4  36856  btwnconn1lem5  36857  btwnconn1lem6  36858  btwnconn1lem7  36859  linethru  36919  lshpkrlem6  40174  athgt  40515  2llnjN  40626  dalaw  40945  cdlemb2  41100  4atexlemex6  41133  cdleme01N  41280  cdleme0ex2N  41283  cdleme7aa  41301  cdleme7e  41306  cdlemg33c0  41761  dihmeetlem3N  42364  pellex  43843