Theorem simp122 1304

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

Assertion

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

Proof of Theorem simp122

Step	Hyp	Ref	Expression
1		simp22 1205	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜓)
2	1	3ad2ant1 1131	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  ax5seglem3  28735  axpasch  28745  exatleN  38866  ps-2b  38944  3atlem1  38945  3atlem2  38946  3atlem4  38948  3atlem5  38949  3atlem6  38950  2llnjaN  39028  4atlem12b  39073  2lplnja  39081  dalemqea  39089  dath2  39199  lneq2at  39240  llnexchb2  39331  dalawlem1  39333  lhpexle3lem  39473  cdleme26ee  39822  cdlemg34  40174  cdlemg35  40175  cdlemg36  40176  cdlemj1  40283  cdlemj2  40284  cdlemk23-3  40364  cdlemk25-3  40366  cdlemk26b-3  40367  cdlemk26-3  40368  cdleml3N  40440  iscnrm3llem2  47941