Theorem simp123 1326

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

Assertion

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

Proof of Theorem simp123

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ax5seglem3  29262  axpasch  29272  exatleN  40159  ps-2b  40237  3atlem1  40238  3atlem2  40239  3atlem4  40241  3atlem5  40242  3atlem6  40243  2llnjaN  40321  2llnjN  40322  4atlem12b  40366  2lplnja  40374  2lplnj  40375  dalemrea  40383  dath2  40492  lneq2at  40533  osumcllem7N  40717  cdleme26ee  41115  cdlemg35  41468  cdlemg36  41469  cdlemj1  41576  cdlemk23-3  41657  cdlemk25-3  41659  cdlemk26b-3  41660  cdlemk27-3  41662  cdlemk28-3  41663  cdleml3N  41733  iscnrm3llem2  49711