Theorem simp123 1324

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

Assertion

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

Proof of Theorem simp123

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 1103

This theorem is referenced by:  ax5seglem3  29218  axpasch  29228  exatleN  40063  ps-2b  40141  3atlem1  40142  3atlem2  40143  3atlem4  40145  3atlem5  40146  3atlem6  40147  2llnjaN  40225  2llnjN  40226  4atlem12b  40270  2lplnja  40278  2lplnj  40279  dalemrea  40287  dath2  40396  lneq2at  40437  osumcllem7N  40621  cdleme26ee  41019  cdlemg35  41372  cdlemg36  41373  cdlemj1  41480  cdlemk23-3  41561  cdlemk25-3  41563  cdlemk26b-3  41564  cdlemk27-3  41566  cdlemk28-3  41567  cdleml3N  41637  iscnrm3llem2  49606