Theorem simp131 1325

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

Assertion

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

Proof of Theorem simp131

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 1103

This theorem is referenced by:  ax5seglem3  29222  exatleN  40068  3atlem1  40147  3atlem2  40148  3atlem5  40151  2llnjaN  40230  4atlem11b  40272  4atlem12b  40275  lplncvrlvol2  40279  dalemsea  40293  dath2  40401  cdlemblem  40457  dalawlem1  40535  lhpexle3lem  40675  4atexlemex6  40738  cdleme22f2  41011  cdleme22g  41012  cdlemg7aN  41289  cdlemg34  41376  cdlemj1  41485  cdlemk23-3  41566  cdlemk25-3  41568  cdlemk26b-3  41569  cdleml3N  41642