Theorem simp131 1393

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

Assertion

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

Proof of Theorem simp131

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

Syntax hints:   → wi 4   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  ax5seglem3  26031  exatleN  35211  3atlem1  35290  3atlem2  35291  3atlem5  35294  2llnjaN  35373  4atlem11b  35415  4atlem12b  35418  lplncvrlvol2  35422  dalemsea  35436  dath2  35544  cdlemblem  35600  dalawlem1  35678  lhpexle3lem  35818  4atexlemex6  35881  cdleme22f2  36155  cdleme22g  36156  cdlemg7aN  36433  cdlemg34  36520  cdlemj1  36629  cdlemk23-3  36710  cdlemk25-3  36712  cdlemk26b-3  36713  cdleml3N  36786