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  29502  axpasch  29512  exatleN  40441  ps-2b  40519  3atlem1  40520  3atlem2  40521  3atlem4  40523  3atlem5  40524  3atlem6  40525  2llnjaN  40603  4atlem12b  40648  2lplnja  40656  dalemqea  40664  dath2  40774  lneq2at  40815  llnexchb2  40906  dalawlem1  40908  lhpexle3lem  41048  cdleme26ee  41397  cdlemg34  41749  cdlemg35  41750  cdlemg36  41751  cdlemj1  41858  cdlemj2  41859  cdlemk23-3  41939  cdlemk25-3  41941  cdlemk26b-3  41942  cdlemk26-3  41943  cdleml3N  42015  iscnrm3llem2  50027