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  29491  axpasch  29501  exatleN  40429  ps-2b  40507  3atlem1  40508  3atlem2  40509  3atlem4  40511  3atlem5  40512  3atlem6  40513  2llnjaN  40591  4atlem12b  40636  2lplnja  40644  dalempea  40651  dath2  40762  lneq2at  40803  llnexchb2  40894  dalawlem1  40896  osumcllem7N  40987  lhpexle3lem  41036  cdleme26ee  41385  cdlemg34  41737  cdlemg36  41739  cdlemj1  41846  cdlemj2  41847  cdlemk23-3  41927  cdlemk25-3  41929  cdlemk26b-3  41930  cdlemk26-3  41931  cdlemk27-3  41932  cdleml3N  42003  iscnrm3llem2  50002