Theorem simp122 1325

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

Assertion

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

Proof of Theorem simp122

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ax5seglem3  29566  axpasch  29576  exatleN  40727  ps-2b  40805  3atlem1  40806  3atlem2  40807  3atlem4  40809  3atlem5  40810  3atlem6  40811  2llnjaN  40889  4atlem12b  40934  2lplnja  40942  dalemqea  40950  dath2  41060  lneq2at  41101  llnexchb2  41192  dalawlem1  41194  lhpexle3lem  41334  cdleme26ee  41683  cdlemg34  42035  cdlemg35  42036  cdlemg36  42037  cdlemj1  42144  cdlemj2  42145  cdlemk23-3  42225  cdlemk25-3  42227  cdlemk26b-3  42228  cdlemk26-3  42229  cdleml3N  42301  iscnrm3llem2  50395