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  29389  exatleN  40278  3atlem1  40357  3atlem2  40358  3atlem5  40361  2llnjaN  40440  4atlem11b  40482  4atlem12b  40485  lplncvrlvol2  40489  dalemsea  40503  dath2  40611  cdlemblem  40667  dalawlem1  40745  lhpexle3lem  40885  4atexlemex6  40948  cdleme22f2  41221  cdleme22g  41222  cdlemg7aN  41499  cdlemg34  41586  cdlemj1  41695  cdlemk23-3  41776  cdlemk25-3  41778  cdlemk26b-3  41779  cdleml3N  41852