Theorem simp131 1307

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

Assertion

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

Proof of Theorem simp131

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  ax5seglem3  27299  exatleN  37418  3atlem1  37497  3atlem2  37498  3atlem5  37501  2llnjaN  37580  4atlem11b  37622  4atlem12b  37625  lplncvrlvol2  37629  dalemsea  37643  dath2  37751  cdlemblem  37807  dalawlem1  37885  lhpexle3lem  38025  4atexlemex6  38088  cdleme22f2  38361  cdleme22g  38362  cdlemg7aN  38639  cdlemg34  38726  cdlemj1  38835  cdlemk23-3  38916  cdlemk25-3  38918  cdlemk26b-3  38919  cdleml3N  38992