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 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ax5seglem3  29566  axpasch  29576  exatleN  40727  ps-2b  40805  3atlem1  40806  3atlem2  40807  3atlem4  40809  3atlem5  40810  3atlem6  40811  2llnjaN  40889  2llnjN  40890  4atlem12b  40934  2lplnja  40942  2lplnj  40943  dalemrea  40951  dath2  41060  lneq2at  41101  osumcllem7N  41285  cdleme26ee  41683  cdlemg35  42036  cdlemg36  42037  cdlemj1  42144  cdlemk23-3  42225  cdlemk25-3  42227  cdlemk26b-3  42228  cdlemk27-3  42230  cdlemk28-3  42231  cdleml3N  42301  iscnrm3llem2  50395