Theorem simp122 1319

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

Assertion

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

Proof of Theorem simp122

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ax5seglem3  29089  axpasch  29099  exatleN  39989  ps-2b  40067  3atlem1  40068  3atlem2  40069  3atlem4  40071  3atlem5  40072  3atlem6  40073  2llnjaN  40151  4atlem12b  40196  2lplnja  40204  dalemqea  40212  dath2  40322  lneq2at  40363  llnexchb2  40454  dalawlem1  40456  lhpexle3lem  40596  cdleme26ee  40945  cdlemg34  41297  cdlemg35  41298  cdlemg36  41299  cdlemj1  41406  cdlemj2  41407  cdlemk23-3  41487  cdlemk25-3  41489  cdlemk26b-3  41490  cdlemk26-3  41491  cdleml3N  41563  iscnrm3llem2  49532