Theorem simp133 1306

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

Assertion

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

Proof of Theorem simp133

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  tsmsxp  22765  ax5seglem3  26719  exatleN  36542  3atlem1  36621  3atlem2  36622  3atlem6  36626  4atlem11b  36746  4atlem12b  36749  lplncvrlvol2  36753  dalemuea  36769  dath2  36875  4atexlemex6  37212  cdleme22f2  37485  cdleme22g  37486  cdlemg7aN  37763  cdlemg31c  37837  cdlemg36  37852  cdlemj1  37959  cdlemj2  37960  cdlemk23-3  38040  cdlemk26b-3  38043