Theorem simp132 1307

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

Assertion

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

Proof of Theorem simp132

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  ax5seglem3  28456  3atlem1  38657  3atlem2  38658  3atlem5  38661  2llnjaN  38740  4atlem11b  38782  4atlem12b  38785  lplncvrlvol2  38789  dalemtea  38804  dath2  38911  cdlemblem  38967  dalawlem1  39045  lhpexle3lem  39185  4atexlemex6  39248  cdleme22f2  39521  cdleme22g  39522  cdlemg7aN  39799  cdlemg34  39886  cdlemj1  39995  cdlemk23-3  40076  cdlemk25-3  40078  cdlemk26b-3  40079