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  29310  axpasch  29320  exatleN  40211  ps-2b  40289  3atlem1  40290  3atlem2  40291  3atlem4  40293  3atlem5  40294  3atlem6  40295  2llnjaN  40373  4atlem12b  40418  2lplnja  40426  dalemqea  40434  dath2  40544  lneq2at  40585  llnexchb2  40676  dalawlem1  40678  lhpexle3lem  40818  cdleme26ee  41167  cdlemg34  41519  cdlemg35  41520  cdlemg36  41521  cdlemj1  41628  cdlemj2  41629  cdlemk23-3  41709  cdlemk25-3  41711  cdlemk26b-3  41712  cdlemk26-3  41713  cdleml3N  41785  iscnrm3llem2  49761