Theorem simp122 1307

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

Assertion

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

Proof of Theorem simp122

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ax5seglem3  28930  axpasch  28940  exatleN  39576  ps-2b  39654  3atlem1  39655  3atlem2  39656  3atlem4  39658  3atlem5  39659  3atlem6  39660  2llnjaN  39738  4atlem12b  39783  2lplnja  39791  dalemqea  39799  dath2  39909  lneq2at  39950  llnexchb2  40041  dalawlem1  40043  lhpexle3lem  40183  cdleme26ee  40532  cdlemg34  40884  cdlemg35  40885  cdlemg36  40886  cdlemj1  40993  cdlemj2  40994  cdlemk23-3  41074  cdlemk25-3  41076  cdlemk26b-3  41077  cdlemk26-3  41078  cdleml3N  41150  iscnrm3llem2  49111