Theorem simp122 1308

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

Assertion

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

Proof of Theorem simp122

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  ax5seglem3  29022  axpasch  29032  exatleN  39809  ps-2b  39887  3atlem1  39888  3atlem2  39889  3atlem4  39891  3atlem5  39892  3atlem6  39893  2llnjaN  39971  4atlem12b  40016  2lplnja  40024  dalemqea  40032  dath2  40142  lneq2at  40183  llnexchb2  40274  dalawlem1  40276  lhpexle3lem  40416  cdleme26ee  40765  cdlemg34  41117  cdlemg35  41118  cdlemg36  41119  cdlemj1  41226  cdlemj2  41227  cdlemk23-3  41307  cdlemk25-3  41309  cdlemk26b-3  41310  cdlemk26-3  41311  cdleml3N  41383  iscnrm3llem2  49338