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 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ax5seglem3  29281  exatleN  40198  3atlem1  40277  3atlem2  40278  3atlem5  40281  2llnjaN  40360  4atlem11b  40402  4atlem12b  40405  lplncvrlvol2  40409  dalemsea  40423  dath2  40531  cdlemblem  40587  dalawlem1  40665  lhpexle3lem  40805  4atexlemex6  40868  cdleme22f2  41141  cdleme22g  41142  cdlemg7aN  41419  cdlemg34  41506  cdlemj1  41615  cdlemk23-3  41696  cdlemk25-3  41698  cdlemk26b-3  41699  cdleml3N  41772