Theorem simp133 1327

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

Assertion

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

Proof of Theorem simp133

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  tsmsxp  24277  ax5seglem3  29218  exatleN  40063  3atlem1  40142  3atlem2  40143  3atlem6  40147  4atlem11b  40267  4atlem12b  40270  lplncvrlvol2  40274  dalemuea  40290  dath2  40396  4atexlemex6  40733  cdleme22f2  41006  cdleme22g  41007  cdlemg7aN  41284  cdlemg31c  41358  cdlemg36  41373  cdlemj1  41480  cdlemj2  41481  cdlemk23-3  41561  cdlemk26b-3  41564