Theorem simp123 1320

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

Assertion

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

Proof of Theorem simp123

Step	Hyp	Ref	Expression
1		simp23 1221	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜒)
2	1	3ad2ant1 1145	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  ax5seglem3  29089  axpasch  29099  exatleN  39989  ps-2b  40067  3atlem1  40068  3atlem2  40069  3atlem4  40071  3atlem5  40072  3atlem6  40073  2llnjaN  40151  2llnjN  40152  4atlem12b  40196  2lplnja  40204  2lplnj  40205  dalemrea  40213  dath2  40322  lneq2at  40363  osumcllem7N  40547  cdleme26ee  40945  cdlemg35  41298  cdlemg36  41299  cdlemj1  41406  cdlemk23-3  41487  cdlemk25-3  41489  cdlemk26b-3  41490  cdlemk27-3  41492  cdlemk28-3  41493  cdleml3N  41563  iscnrm3llem2  49532