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 210  df-an 400  df-3an 1086

This theorem is referenced by:  tsmsxp  22760  ax5seglem3  26725  exatleN  36700  3atlem1  36779  3atlem2  36780  3atlem6  36784  4atlem11b  36904  4atlem12b  36907  lplncvrlvol2  36911  dalemuea  36927  dath2  37033  4atexlemex6  37370  cdleme22f2  37643  cdleme22g  37644  cdlemg7aN  37921  cdlemg31c  37995  cdlemg36  38010  cdlemj1  38117  cdlemj2  38118  cdlemk23-3  38198  cdlemk26b-3  38201