Theorem simp131 1306

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

Assertion

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

Proof of Theorem simp131

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  ax5seglem3  28456  exatleN  38578  3atlem1  38657  3atlem2  38658  3atlem5  38661  2llnjaN  38740  4atlem11b  38782  4atlem12b  38785  lplncvrlvol2  38789  dalemsea  38803  dath2  38911  cdlemblem  38967  dalawlem1  39045  lhpexle3lem  39185  4atexlemex6  39248  cdleme22f2  39521  cdleme22g  39522  cdlemg7aN  39799  cdlemg34  39886  cdlemj1  39995  cdlemk23-3  40076  cdlemk25-3  40078  cdlemk26b-3  40079  cdleml3N  40152