Theorem simp122 1303

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

Assertion

Ref	Expression
simp122	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓)

Proof of Theorem simp122

Step	Hyp	Ref	Expression
1		simp22 1204	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜓)
2	1	3ad2ant1 1130	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  ax5seglem3  28624  axpasch  28634  exatleN  38731  ps-2b  38809  3atlem1  38810  3atlem2  38811  3atlem4  38813  3atlem5  38814  3atlem6  38815  2llnjaN  38893  4atlem12b  38938  2lplnja  38946  dalemqea  38954  dath2  39064  lneq2at  39105  llnexchb2  39196  dalawlem1  39198  lhpexle3lem  39338  cdleme26ee  39687  cdlemg34  40039  cdlemg35  40040  cdlemg36  40041  cdlemj1  40148  cdlemj2  40149  cdlemk23-3  40229  cdlemk25-3  40231  cdlemk26b-3  40232  cdlemk26-3  40233  cdleml3N  40305  iscnrm3llem2  47737