Theorem simp132 1311

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

Assertion

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

Proof of Theorem simp132

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ax5seglem3  29000  3atlem1  39929  3atlem2  39930  3atlem5  39933  2llnjaN  40012  4atlem11b  40054  4atlem12b  40057  lplncvrlvol2  40061  dalemtea  40076  dath2  40183  cdlemblem  40239  dalawlem1  40317  lhpexle3lem  40457  4atexlemex6  40520  cdleme22f2  40793  cdleme22g  40794  cdlemg7aN  41071  cdlemg34  41158  cdlemj1  41267  cdlemk23-3  41348  cdlemk25-3  41350  cdlemk26b-3  41351