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 210  df-an 400  df-3an 1086

This theorem is referenced by:  ax5seglem3  26725  axpasch  26735  exatleN  36700  ps-2b  36778  3atlem1  36779  3atlem2  36780  3atlem4  36782  3atlem5  36783  3atlem6  36784  2llnjaN  36862  4atlem12b  36907  2lplnja  36915  dalemqea  36923  dath2  37033  lneq2at  37074  llnexchb2  37165  dalawlem1  37167  lhpexle3lem  37307  cdleme26ee  37656  cdlemg34  38008  cdlemg35  38009  cdlemg36  38010  cdlemj1  38117  cdlemj2  38118  cdlemk23-3  38198  cdlemk25-3  38200  cdlemk26b-3  38201  cdlemk26-3  38202  cdleml3N  38274