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  29388  axpasch  29398  exatleN  40277  ps-2b  40355  3atlem1  40356  3atlem2  40357  3atlem4  40359  3atlem5  40360  3atlem6  40361  2llnjaN  40439  2llnjN  40440  4atlem12b  40484  2lplnja  40492  2lplnj  40493  dalemrea  40501  dath2  40610  lneq2at  40651  osumcllem7N  40835  cdleme26ee  41233  cdlemg35  41586  cdlemg36  41587  cdlemj1  41694  cdlemk23-3  41775  cdlemk25-3  41777  cdlemk26b-3  41778  cdlemk27-3  41780  cdlemk28-3  41781  cdleml3N  41851  iscnrm3llem2  49876