Theorem simp123 1392

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

Assertion

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

Proof of Theorem simp123

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

Syntax hints:   → wi 4   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  ax5seglem3  26031  axpasch  26041  exatleN  35211  ps-2b  35289  3atlem1  35290  3atlem2  35291  3atlem4  35293  3atlem5  35294  3atlem6  35295  2llnjaN  35373  2llnjN  35374  4atlem12b  35418  2lplnja  35426  2lplnj  35427  dalemrea  35435  dath2  35544  lneq2at  35585  osumcllem7N  35769  cdleme26ee  36168  cdlemg35  36521  cdlemg36  36522  cdlemj1  36629  cdlemk23-3  36710  cdlemk25-3  36712  cdlemk26b-3  36713  cdlemk27-3  36715  cdlemk28-3  36716  cdleml3N  36786