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  29509  exatleN  40461  3atlem1  40540  3atlem2  40541  3atlem5  40544  2llnjaN  40623  4atlem11b  40665  4atlem12b  40668  lplncvrlvol2  40672  dalemsea  40686  dath2  40794  cdlemblem  40850  dalawlem1  40928  lhpexle3lem  41068  4atexlemex6  41131  cdleme22f2  41404  cdleme22g  41405  cdlemg7aN  41682  cdlemg34  41769  cdlemj1  41878  cdlemk23-3  41959  cdlemk25-3  41961  cdlemk26b-3  41962  cdleml3N  42035