Theorem simp133 1323

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

Assertion

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

Proof of Theorem simp133

Step	Hyp	Ref	Expression
1		simp33 1224	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒)
2	1	3ad2ant1 1145	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  tsmsxp  24203  ax5seglem3  29089  exatleN  39989  3atlem1  40068  3atlem2  40069  3atlem6  40073  4atlem11b  40193  4atlem12b  40196  lplncvrlvol2  40200  dalemuea  40216  dath2  40322  4atexlemex6  40659  cdleme22f2  40932  cdleme22g  40933  cdlemg7aN  41210  cdlemg31c  41284  cdlemg36  41299  cdlemj1  41406  cdlemj2  41407  cdlemk23-3  41487  cdlemk26b-3  41490