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  29310  axpasch  29320  exatleN  40211  ps-2b  40289  3atlem1  40290  3atlem2  40291  3atlem4  40293  3atlem5  40294  3atlem6  40295  2llnjaN  40373  2llnjN  40374  4atlem12b  40418  2lplnja  40426  2lplnj  40427  dalemrea  40435  dath2  40544  lneq2at  40585  osumcllem7N  40769  cdleme26ee  41167  cdlemg35  41520  cdlemg36  41521  cdlemj1  41628  cdlemk23-3  41709  cdlemk25-3  41711  cdlemk26b-3  41712  cdlemk27-3  41714  cdlemk28-3  41715  cdleml3N  41785  iscnrm3llem2  49761