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  39449  ps-2b  39527  3atlem1  39528  3atlem2  39529  3atlem4  39531  3atlem5  39532  3atlem6  39533  2llnjaN  39611  2llnjN  39612  4atlem12b  39656  2lplnja  39664  2lplnj  39665  dalemrea  39673  dath2  39782  lneq2at  39823  osumcllem7N  40007  cdleme26ee  40405  cdlemg35  40758  cdlemg36  40759  cdlemj1  40866  cdlemk23-3  40947  cdlemk25-3  40949  cdlemk26b-3  40950  cdlemk27-3  40952  cdlemk28-3  40953  cdleml3N  41023  iscnrm3llem2  48987