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 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1103

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 1105

This theorem is referenced by:  tsmsxp  24293  ax5seglem3  29262  exatleN  40159  3atlem1  40238  3atlem2  40239  3atlem6  40243  4atlem11b  40363  4atlem12b  40366  lplncvrlvol2  40370  dalemuea  40386  dath2  40492  4atexlemex6  40829  cdleme22f2  41102  cdleme22g  41103  cdlemg7aN  41380  cdlemg31c  41454  cdlemg36  41469  cdlemj1  41576  cdlemj2  41577  cdlemk23-3  41657  cdlemk26b-3  41660