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  24381  ax5seglem3  29388  exatleN  40277  3atlem1  40356  3atlem2  40357  3atlem6  40361  4atlem11b  40481  4atlem12b  40484  lplncvrlvol2  40488  dalemuea  40504  dath2  40610  4atexlemex6  40947  cdleme22f2  41220  cdleme22g  41221  cdlemg7aN  41498  cdlemg31c  41572  cdlemg36  41587  cdlemj1  41694  cdlemj2  41695  cdlemk23-3  41775  cdlemk26b-3  41778