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  29396  axpasch  29406  exatleN  40285  ps-2b  40363  3atlem1  40364  3atlem2  40365  3atlem4  40367  3atlem5  40368  3atlem6  40369  2llnjaN  40447  4atlem12b  40492  2lplnja  40500  dalempea  40507  dath2  40618  lneq2at  40659  llnexchb2  40750  dalawlem1  40752  osumcllem7N  40843  lhpexle3lem  40892  cdleme26ee  41241  cdlemg34  41593  cdlemg36  41595  cdlemj1  41702  cdlemj2  41703  cdlemk23-3  41783  cdlemk25-3  41785  cdlemk26b-3  41786  cdlemk26-3  41787  cdlemk27-3  41788  cdleml3N  41859  iscnrm3llem2  49884