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 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  ax5seglem3  29262  axpasch  29272  exatleN  40159  ps-2b  40237  3atlem1  40238  3atlem2  40239  3atlem4  40241  3atlem5  40242  3atlem6  40243  2llnjaN  40321  4atlem12b  40366  2lplnja  40374  dalempea  40381  dath2  40492  lneq2at  40533  llnexchb2  40624  dalawlem1  40626  osumcllem7N  40717  lhpexle3lem  40766  cdleme26ee  41115  cdlemg34  41467  cdlemg36  41469  cdlemj1  41576  cdlemj2  41577  cdlemk23-3  41657  cdlemk25-3  41659  cdlemk26b-3  41660  cdlemk26-3  41661  cdlemk27-3  41662  cdleml3N  41733  iscnrm3llem2  49711