Theorem simp132 1190

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

Assertion

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

Proof of Theorem simp132

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

Syntax hints:   → wi 4   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  ax5seglem3  25611  3atlem1  33787  3atlem2  33788  3atlem5  33791  2llnjaN  33870  4atlem11b  33912  4atlem12b  33915  lplncvrlvol2  33919  dalemtea  33934  dath2  34041  cdlemblem  34097  dalawlem1  34175  lhpexle3lem  34315  4atexlemex6  34378  cdleme22f2  34653  cdleme22g  34654  cdlemg7aN  34931  cdlemg34  35018  cdlemj1  35127  cdlemk23-3  35208  cdlemk25-3  35210  cdlemk26b-3  35211