Theorem simp123 1308

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

Assertion

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

Proof of Theorem simp123

Step	Hyp	Ref	Expression
1		simp23 1209	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜒)
2	1	3ad2ant1 1133	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ax5seglem3  28910  axpasch  28920  exatleN  39423  ps-2b  39501  3atlem1  39502  3atlem2  39503  3atlem4  39505  3atlem5  39506  3atlem6  39507  2llnjaN  39585  2llnjN  39586  4atlem12b  39630  2lplnja  39638  2lplnj  39639  dalemrea  39647  dath2  39756  lneq2at  39797  osumcllem7N  39981  cdleme26ee  40379  cdlemg35  40732  cdlemg36  40733  cdlemj1  40840  cdlemk23-3  40921  cdlemk25-3  40923  cdlemk26b-3  40924  cdlemk27-3  40926  cdlemk28-3  40927  cdleml3N  40997  iscnrm3llem2  48924