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  29004  axpasch  29014  exatleN  39664  ps-2b  39742  3atlem1  39743  3atlem2  39744  3atlem4  39746  3atlem5  39747  3atlem6  39748  2llnjaN  39826  4atlem12b  39871  2lplnja  39879  dalemqea  39887  dath2  39997  lneq2at  40038  llnexchb2  40129  dalawlem1  40131  lhpexle3lem  40271  cdleme26ee  40620  cdlemg34  40972  cdlemg35  40973  cdlemg36  40974  cdlemj1  41081  cdlemj2  41082  cdlemk23-3  41162  cdlemk25-3  41164  cdlemk26b-3  41165  cdlemk26-3  41166  cdleml3N  41238  iscnrm3llem2  49195