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  29515  axpasch  29525  exatleN  40555  ps-2b  40633  3atlem1  40634  3atlem2  40635  3atlem4  40637  3atlem5  40638  3atlem6  40639  2llnjaN  40717  4atlem12b  40762  2lplnja  40770  dalempea  40777  dath2  40888  lneq2at  40929  llnexchb2  41020  dalawlem1  41022  osumcllem7N  41113  lhpexle3lem  41162  cdleme26ee  41511  cdlemg34  41863  cdlemg36  41865  cdlemj1  41972  cdlemj2  41973  cdlemk23-3  42053  cdlemk25-3  42055  cdlemk26b-3  42056  cdlemk26-3  42057  cdlemk27-3  42058  cdleml3N  42129  iscnrm3llem2  50158