Theorem simp133 1394

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

Assertion

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

Proof of Theorem simp133

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

Syntax hints:   → wi 4   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  tsmsxp  22178  ax5seglem3  26032  exatleN  35212  3atlem1  35291  3atlem2  35292  3atlem6  35296  4atlem11b  35416  4atlem12b  35419  lplncvrlvol2  35423  dalemuea  35439  dath2  35545  4atexlemex6  35882  cdleme22f2  36156  cdleme22g  36157  cdlemg7aN  36434  cdlemg31c  36508  cdlemg36  36523  cdlemj1  36630  cdlemj2  36631  cdlemk23-3  36711  cdlemk26b-3  36714