Theorem simp131 1327

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

Assertion

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

Proof of Theorem simp131

Step	Hyp	Ref	Expression
1		simp31 1228	. 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  29566  exatleN  40727  3atlem1  40806  3atlem2  40807  3atlem5  40810  2llnjaN  40889  4atlem11b  40931  4atlem12b  40934  lplncvrlvol2  40938  dalemsea  40952  dath2  41060  cdlemblem  41116  dalawlem1  41194  lhpexle3lem  41334  4atexlemex6  41397  cdleme22f2  41670  cdleme22g  41671  cdlemg7aN  41948  cdlemg34  42035  cdlemj1  42144  cdlemk23-3  42225  cdlemk25-3  42227  cdlemk26b-3  42228  cdleml3N  42301