Theorem simp131 1305

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

Assertion

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

Proof of Theorem simp131

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  ax5seglem3  26725  exatleN  36700  3atlem1  36779  3atlem2  36780  3atlem5  36783  2llnjaN  36862  4atlem11b  36904  4atlem12b  36907  lplncvrlvol2  36911  dalemsea  36925  dath2  37033  cdlemblem  37089  dalawlem1  37167  lhpexle3lem  37307  4atexlemex6  37370  cdleme22f2  37643  cdleme22g  37644  cdlemg7aN  37921  cdlemg34  38008  cdlemj1  38117  cdlemk23-3  38198  cdlemk25-3  38200  cdlemk26b-3  38201  cdleml3N  38274