Theorem simp133 1317

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

Assertion

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

Proof of Theorem simp133

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  tsmsxp  24138  ax5seglem3  29018  exatleN  39896  3atlem1  39975  3atlem2  39976  3atlem6  39980  4atlem11b  40100  4atlem12b  40103  lplncvrlvol2  40107  dalemuea  40123  dath2  40229  4atexlemex6  40566  cdleme22f2  40839  cdleme22g  40840  cdlemg7aN  41117  cdlemg31c  41191  cdlemg36  41206  cdlemj1  41313  cdlemj2  41314  cdlemk23-3  41394  cdlemk26b-3  41397