Theorem simp133 1329

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

Assertion

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

Proof of Theorem simp133

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  tsmsxp  24529  ax5seglem3  29566  exatleN  40727  3atlem1  40806  3atlem2  40807  3atlem6  40811  4atlem11b  40931  4atlem12b  40934  lplncvrlvol2  40938  dalemuea  40954  dath2  41060  4atexlemex6  41397  cdleme22f2  41670  cdleme22g  41671  cdlemg7aN  41948  cdlemg31c  42022  cdlemg36  42037  cdlemj1  42144  cdlemj2  42145  cdlemk23-3  42225  cdlemk26b-3  42228