Theorem simp132 1327

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

Assertion

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

Proof of Theorem simp132

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

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

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 401  df-3an 1104

This theorem is used by:  ax5seglem3  29292  3atlem1  40285  3atlem2  40286  3atlem5  40289  2llnjaN  40368  4atlem11b  40410  4atlem12b  40413  lplncvrlvol2  40417  dalemtea  40432  dath2  40539  cdlemblem  40595  dalawlem1  40673  lhpexle3lem  40813  4atexlemex6  40876  cdleme22f2  41149  cdleme22g  41150  cdlemg7aN  41427  cdlemg34  41514  cdlemj1  41623  cdlemk23-3  41704  cdlemk25-3  41706  cdlemk26b-3  41707