Theorem simp131 1310

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

Assertion

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

Proof of Theorem simp131

Step	Hyp	Ref	Expression
1		simp31 1211	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑)
2	1	3ad2ant1 1134	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ax5seglem3  29017  exatleN  39867  3atlem1  39946  3atlem2  39947  3atlem5  39950  2llnjaN  40029  4atlem11b  40071  4atlem12b  40074  lplncvrlvol2  40078  dalemsea  40092  dath2  40200  cdlemblem  40256  dalawlem1  40334  lhpexle3lem  40474  4atexlemex6  40537  cdleme22f2  40810  cdleme22g  40811  cdlemg7aN  41088  cdlemg34  41175  cdlemj1  41284  cdlemk23-3  41365  cdlemk25-3  41367  cdlemk26b-3  41368  cdleml3N  41441