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  29514  3atlem1  40633  3atlem2  40634  3atlem5  40637  2llnjaN  40716  4atlem11b  40758  4atlem12b  40761  lplncvrlvol2  40765  dalemtea  40780  dath2  40887  cdlemblem  40943  dalawlem1  41021  lhpexle3lem  41161  4atexlemex6  41224  cdleme22f2  41497  cdleme22g  41498  cdlemg7aN  41775  cdlemg34  41862  cdlemj1  41971  cdlemk23-3  42052  cdlemk25-3  42054  cdlemk26b-3  42055