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  29518  exatleN  40598  3atlem1  40677  3atlem2  40678  3atlem5  40681  2llnjaN  40760  4atlem11b  40802  4atlem12b  40805  lplncvrlvol2  40809  dalemsea  40823  dath2  40931  cdlemblem  40987  dalawlem1  41065  lhpexle3lem  41205  4atexlemex6  41268  cdleme22f2  41541  cdleme22g  41542  cdlemg7aN  41819  cdlemg34  41906  cdlemj1  42015  cdlemk23-3  42096  cdlemk25-3  42098  cdlemk26b-3  42099  cdleml3N  42172