Theorem simp132 1308

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

Assertion

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

Proof of Theorem simp132

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ax5seglem3  27299  3atlem1  37497  3atlem2  37498  3atlem5  37501  2llnjaN  37580  4atlem11b  37622  4atlem12b  37625  lplncvrlvol2  37629  dalemtea  37644  dath2  37751  cdlemblem  37807  dalawlem1  37885  lhpexle3lem  38025  4atexlemex6  38088  cdleme22f2  38361  cdleme22g  38362  cdlemg7aN  38639  cdlemg34  38726  cdlemj1  38835  cdlemk23-3  38916  cdlemk25-3  38918  cdlemk26b-3  38919