Theorem simp121 1324

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

Assertion

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

Proof of Theorem simp121

Step	Hyp	Ref	Expression
1		simp21 1225	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜑)
2	1	3ad2ant1 1151	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ax5seglem3  29318  axpasch  29328  exatleN  40219  ps-2b  40297  3atlem1  40298  3atlem2  40299  3atlem4  40301  3atlem5  40302  3atlem6  40303  2llnjaN  40381  4atlem12b  40426  2lplnja  40434  dalempea  40441  dath2  40552  lneq2at  40593  llnexchb2  40684  dalawlem1  40686  osumcllem7N  40777  lhpexle3lem  40826  cdleme26ee  41175  cdlemg34  41527  cdlemg36  41529  cdlemj1  41636  cdlemj2  41637  cdlemk23-3  41717  cdlemk25-3  41719  cdlemk26b-3  41720  cdlemk26-3  41721  cdlemk27-3  41722  cdleml3N  41793  iscnrm3llem2  49769