Theorem simp122 1325

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

Assertion

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

Proof of Theorem simp122

Step	Hyp	Ref	Expression
1		simp22 1226	. 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  4atlem12b  40484  2lplnja  40492  dalemqea  40500  dath2  40610  lneq2at  40651  llnexchb2  40742  dalawlem1  40744  lhpexle3lem  40884  cdleme26ee  41233  cdlemg34  41585  cdlemg35  41586  cdlemg36  41587  cdlemj1  41694  cdlemj2  41695  cdlemk23-3  41775  cdlemk25-3  41777  cdlemk26b-3  41778  cdlemk26-3  41779  cdleml3N  41851  iscnrm3llem2  49876