Theorem simp2lr 1129

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

Assertion

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

Proof of Theorem simp2lr

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  tfrlem5  7476  omeu  7665  4sqlem18  15666  vdwlem10  15694  mvrf1  19425  mdetuni0  20427  mdetmul  20429  tsmsxp  21958  ax5seglem3  25811  btwnconn1lem1  32194  btwnconn1lem3  32196  btwnconn1lem4  32197  btwnconn1lem5  32198  btwnconn1lem6  32199  btwnconn1lem7  32200  linethru  32260  lshpkrlem6  34402  athgt  34742  2llnjN  34853  dalaw  35172  cdlemb2  35327  4atexlemex6  35360  cdleme01N  35508  cdleme0ex2N  35511  cdleme7aa  35529  cdleme7e  35534  cdlemg33c0  35990  dihmeetlem3N  36594  pellex  37399  expmordi  37512