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  24341  ax5seglem3  29310  exatleN  40211  3atlem1  40290  3atlem2  40291  3atlem6  40295  4atlem11b  40415  4atlem12b  40418  lplncvrlvol2  40422  dalemuea  40438  dath2  40544  4atexlemex6  40881  cdleme22f2  41154  cdleme22g  41155  cdlemg7aN  41432  cdlemg31c  41506  cdlemg36  41521  cdlemj1  41628  cdlemj2  41629  cdlemk23-3  41709  cdlemk26b-3  41712