Theorem simp132 1316

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

Assertion

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

Proof of Theorem simp132

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ax5seglem3  29025  3atlem1  39982  3atlem2  39983  3atlem5  39986  2llnjaN  40065  4atlem11b  40107  4atlem12b  40110  lplncvrlvol2  40114  dalemtea  40129  dath2  40236  cdlemblem  40292  dalawlem1  40370  lhpexle3lem  40510  4atexlemex6  40573  cdleme22f2  40846  cdleme22g  40847  cdlemg7aN  41124  cdlemg34  41211  cdlemj1  41320  cdlemk23-3  41401  cdlemk25-3  41403  cdlemk26b-3  41404