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  29491  3atlem1  40508  3atlem2  40509  3atlem5  40512  2llnjaN  40591  4atlem11b  40633  4atlem12b  40636  lplncvrlvol2  40640  dalemtea  40655  dath2  40762  cdlemblem  40818  dalawlem1  40896  lhpexle3lem  41036  4atexlemex6  41099  cdleme22f2  41372  cdleme22g  41373  cdlemg7aN  41650  cdlemg34  41737  cdlemj1  41846  cdlemk23-3  41927  cdlemk25-3  41929  cdlemk26b-3  41930