Theorem simp132 1310

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

Assertion

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

Proof of Theorem simp132

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  ax5seglem3  26877  3atlem1  37140  3atlem2  37141  3atlem5  37144  2llnjaN  37223  4atlem11b  37265  4atlem12b  37268  lplncvrlvol2  37272  dalemtea  37287  dath2  37394  cdlemblem  37450  dalawlem1  37528  lhpexle3lem  37668  4atexlemex6  37731  cdleme22f2  38004  cdleme22g  38005  cdlemg7aN  38282  cdlemg34  38369  cdlemj1  38478  cdlemk23-3  38559  cdlemk25-3  38561  cdlemk26b-3  38562