Theorem simp122 1305

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

Assertion

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

Proof of Theorem simp122

Step	Hyp	Ref	Expression
1		simp22 1206	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜓)
2	1	3ad2ant1 1132	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ax5seglem3  27299  axpasch  27309  exatleN  37418  ps-2b  37496  3atlem1  37497  3atlem2  37498  3atlem4  37500  3atlem5  37501  3atlem6  37502  2llnjaN  37580  4atlem12b  37625  2lplnja  37633  dalemqea  37641  dath2  37751  lneq2at  37792  llnexchb2  37883  dalawlem1  37885  lhpexle3lem  38025  cdleme26ee  38374  cdlemg34  38726  cdlemg35  38727  cdlemg36  38728  cdlemj1  38835  cdlemj2  38836  cdlemk23-3  38916  cdlemk25-3  38918  cdlemk26b-3  38919  cdlemk26-3  38920  cdleml3N  38992  iscnrm3llem2  46244