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  24291  ax5seglem3  29247  exatleN  40124  3atlem1  40203  3atlem2  40204  3atlem6  40208  4atlem11b  40328  4atlem12b  40331  lplncvrlvol2  40335  dalemuea  40351  dath2  40457  4atexlemex6  40794  cdleme22f2  41067  cdleme22g  41068  cdlemg7aN  41345  cdlemg31c  41419  cdlemg36  41434  cdlemj1  41541  cdlemj2  41542  cdlemk23-3  41622  cdlemk26b-3  41625