Theorem simp133 1309

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

Assertion

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

Proof of Theorem simp133

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  tsmsxp  23306  ax5seglem3  27299  exatleN  37418  3atlem1  37497  3atlem2  37498  3atlem6  37502  4atlem11b  37622  4atlem12b  37625  lplncvrlvol2  37629  dalemuea  37645  dath2  37751  4atexlemex6  38088  cdleme22f2  38361  cdleme22g  38362  cdlemg7aN  38639  cdlemg31c  38713  cdlemg36  38728  cdlemj1  38835  cdlemj2  38836  cdlemk23-3  38916  cdlemk26b-3  38919