Theorem simp132 1326

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

Assertion

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

Proof of Theorem simp132

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  ax5seglem3  29190  3atlem1  40119  3atlem2  40120  3atlem5  40123  2llnjaN  40202  4atlem11b  40244  4atlem12b  40247  lplncvrlvol2  40251  dalemtea  40266  dath2  40373  cdlemblem  40429  dalawlem1  40507  lhpexle3lem  40647  4atexlemex6  40710  cdleme22f2  40983  cdleme22g  40984  cdlemg7aN  41261  cdlemg34  41348  cdlemj1  41457  cdlemk23-3  41538  cdlemk25-3  41540  cdlemk26b-3  41541