Theorem simp2lr 1306

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

Assertion

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

Proof of Theorem simp2lr

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1070

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 383  df-3an 1072

This theorem is referenced by:  tfrlem5  7628  omeu  7818  4sqlem18  15872  vdwlem10  15900  mvrf1  19639  mdetuni0  20644  mdetmul  20646  tsmsxp  22177  ax5seglem3  26031  btwnconn1lem1  32525  btwnconn1lem3  32527  btwnconn1lem4  32528  btwnconn1lem5  32529  btwnconn1lem6  32530  btwnconn1lem7  32531  linethru  32591  lshpkrlem6  34917  athgt  35257  2llnjN  35368  dalaw  35687  cdlemb2  35842  4atexlemex6  35875  cdleme01N  36023  cdleme0ex2N  36026  cdleme7aa  36044  cdleme7e  36049  cdlemg33c0  36504  dihmeetlem3N  37108  pellex  37918  expmordi  38031