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

This theorem is referenced by:  ax5seglem3  28909  3atlem1  39581  3atlem2  39582  3atlem5  39585  2llnjaN  39664  4atlem11b  39706  4atlem12b  39709  lplncvrlvol2  39713  dalemtea  39728  dath2  39835  cdlemblem  39891  dalawlem1  39969  lhpexle3lem  40109  4atexlemex6  40172  cdleme22f2  40445  cdleme22g  40446  cdlemg7aN  40723  cdlemg34  40810  cdlemj1  40919  cdlemk23-3  41000  cdlemk25-3  41002  cdlemk26b-3  41003