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 780	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant2 1152	1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  fpr3g  8283  tfrlem5  8367  omeu  8571  expmordi  14205  4sqlem18  17023  vdwlem10  17051  mvrf1  22116  mdetuni0  22759  mdetmul  22761  tsmsxp  24293  ax5seglem3  29259  btwnconn1lem1  36557  btwnconn1lem3  36559  btwnconn1lem4  36560  btwnconn1lem5  36561  btwnconn1lem6  36562  btwnconn1lem7  36563  linethru  36623  lshpkrlem6  39867  athgt  40208  2llnjN  40319  dalaw  40638  cdlemb2  40793  4atexlemex6  40826  cdleme01N  40973  cdleme0ex2N  40976  cdleme7aa  40994  cdleme7e  40999  cdlemg33c0  41454  dihmeetlem3N  42057  pellex  43542