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  29539  3atlem1  40732  3atlem2  40733  3atlem5  40736  2llnjaN  40815  4atlem11b  40857  4atlem12b  40860  lplncvrlvol2  40864  dalemtea  40879  dath2  40986  cdlemblem  41042  dalawlem1  41120  lhpexle3lem  41260  4atexlemex6  41323  cdleme22f2  41596  cdleme22g  41597  cdlemg7aN  41874  cdlemg34  41961  cdlemj1  42070  cdlemk23-3  42151  cdlemk25-3  42153  cdlemk26b-3  42154