Theorem simp123 1306

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

Assertion

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

Proof of Theorem simp123

Step	Hyp	Ref	Expression
1		simp23 1207	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜒)
2	1	3ad2ant1 1132	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ax5seglem3  27299  axpasch  27309  exatleN  37418  ps-2b  37496  3atlem1  37497  3atlem2  37498  3atlem4  37500  3atlem5  37501  3atlem6  37502  2llnjaN  37580  2llnjN  37581  4atlem12b  37625  2lplnja  37633  2lplnj  37634  dalemrea  37642  dath2  37751  lneq2at  37792  osumcllem7N  37976  cdleme26ee  38374  cdlemg35  38727  cdlemg36  38728  cdlemj1  38835  cdlemk23-3  38916  cdlemk25-3  38918  cdlemk26b-3  38919  cdlemk27-3  38921  cdlemk28-3  38922  cdleml3N  38992  iscnrm3llem2  46244