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  24467  ax5seglem3  29502  exatleN  40441  3atlem1  40520  3atlem2  40521  3atlem6  40525  4atlem11b  40645  4atlem12b  40648  lplncvrlvol2  40652  dalemuea  40668  dath2  40774  4atexlemex6  41111  cdleme22f2  41384  cdleme22g  41385  cdlemg7aN  41662  cdlemg31c  41736  cdlemg36  41751  cdlemj1  41858  cdlemj2  41859  cdlemk23-3  41939  cdlemk26b-3  41942