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  29338  exatleN  40238  3atlem1  40317  3atlem2  40318  3atlem5  40321  2llnjaN  40400  4atlem11b  40442  4atlem12b  40445  lplncvrlvol2  40449  dalemsea  40463  dath2  40571  cdlemblem  40627  dalawlem1  40705  lhpexle3lem  40845  4atexlemex6  40908  cdleme22f2  41181  cdleme22g  41182  cdlemg7aN  41459  cdlemg34  41546  cdlemj1  41655  cdlemk23-3  41736  cdlemk25-3  41738  cdlemk26b-3  41739  cdleml3N  41812