Theorem simp133 1307

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

Assertion

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

Proof of Theorem simp133

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 1086

This theorem is referenced by:  tsmsxp  24079  ax5seglem3  28762  exatleN  38909  3atlem1  38988  3atlem2  38989  3atlem6  38993  4atlem11b  39113  4atlem12b  39116  lplncvrlvol2  39120  dalemuea  39136  dath2  39242  4atexlemex6  39579  cdleme22f2  39852  cdleme22g  39853  cdlemg7aN  40130  cdlemg31c  40204  cdlemg36  40219  cdlemj1  40326  cdlemj2  40327  cdlemk23-3  40407  cdlemk26b-3  40410