Theorem simp132 1328

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

Assertion

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

Proof of Theorem simp132

Step	Hyp	Ref	Expression
1		simp32 1229	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓)
2	1	3ad2ant1 1151	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ax5seglem3  29318  3atlem1  40298  3atlem2  40299  3atlem5  40302  2llnjaN  40381  4atlem11b  40423  4atlem12b  40426  lplncvrlvol2  40430  dalemtea  40445  dath2  40552  cdlemblem  40608  dalawlem1  40686  lhpexle3lem  40826  4atexlemex6  40889  cdleme22f2  41162  cdleme22g  41163  cdlemg7aN  41440  cdlemg34  41527  cdlemj1  41636  cdlemk23-3  41717  cdlemk25-3  41719  cdlemk26b-3  41720