Theorem simp122 1323

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

Assertion

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

Proof of Theorem simp122

Step	Hyp	Ref	Expression
1		simp22 1224	. 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  4atlem12b  40270  2lplnja  40278  dalemqea  40286  dath2  40396  lneq2at  40437  llnexchb2  40528  dalawlem1  40530  lhpexle3lem  40670  cdleme26ee  41019  cdlemg34  41371  cdlemg35  41372  cdlemg36  41373  cdlemj1  41480  cdlemj2  41481  cdlemk23-3  41561  cdlemk25-3  41563  cdlemk26b-3  41564  cdlemk26-3  41565  cdleml3N  41637  iscnrm3llem2  49606