Theorem simp133 1311

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

Assertion

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

Proof of Theorem simp133

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  tsmsxp  24090  ax5seglem3  28930  exatleN  39576  3atlem1  39655  3atlem2  39656  3atlem6  39660  4atlem11b  39780  4atlem12b  39783  lplncvrlvol2  39787  dalemuea  39803  dath2  39909  4atexlemex6  40246  cdleme22f2  40519  cdleme22g  40520  cdlemg7aN  40797  cdlemg31c  40871  cdlemg36  40886  cdlemj1  40993  cdlemj2  40994  cdlemk23-3  41074  cdlemk26b-3  41077