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  24481  ax5seglem3  29516  exatleN  40568  3atlem1  40647  3atlem2  40648  3atlem6  40652  4atlem11b  40772  4atlem12b  40775  lplncvrlvol2  40779  dalemuea  40795  dath2  40901  4atexlemex6  41238  cdleme22f2  41511  cdleme22g  41512  cdlemg7aN  41789  cdlemg31c  41863  cdlemg36  41878  cdlemj1  41985  cdlemj2  41986  cdlemk23-3  42066  cdlemk26b-3  42069