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  29396  3atlem1  40364  3atlem2  40365  3atlem5  40368  2llnjaN  40447  4atlem11b  40489  4atlem12b  40492  lplncvrlvol2  40496  dalemtea  40511  dath2  40618  cdlemblem  40674  dalawlem1  40752  lhpexle3lem  40892  4atexlemex6  40955  cdleme22f2  41228  cdleme22g  41229  cdlemg7aN  41506  cdlemg34  41593  cdlemj1  41702  cdlemk23-3  41783  cdlemk25-3  41785  cdlemk26b-3  41786