Theorem simp133 1308

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

Assertion

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

Proof of Theorem simp133

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  tsmsxp  23879  ax5seglem3  28456  exatleN  38578  3atlem1  38657  3atlem2  38658  3atlem6  38662  4atlem11b  38782  4atlem12b  38785  lplncvrlvol2  38789  dalemuea  38805  dath2  38911  4atexlemex6  39248  cdleme22f2  39521  cdleme22g  39522  cdlemg7aN  39799  cdlemg31c  39873  cdlemg36  39888  cdlemj1  39995  cdlemj2  39996  cdlemk23-3  40076  cdlemk26b-3  40079