Theorem simp133 1312

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

Assertion

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

Proof of Theorem simp133

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  tsmsxp  24120  ax5seglem3  29000  exatleN  39850  3atlem1  39929  3atlem2  39930  3atlem6  39934  4atlem11b  40054  4atlem12b  40057  lplncvrlvol2  40061  dalemuea  40077  dath2  40183  4atexlemex6  40520  cdleme22f2  40793  cdleme22g  40794  cdlemg7aN  41071  cdlemg31c  41145  cdlemg36  41160  cdlemj1  41267  cdlemj2  41268  cdlemk23-3  41348  cdlemk26b-3  41351