Theorem simp122 1306

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

Assertion

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

Proof of Theorem simp122

Step	Hyp	Ref	Expression
1		simp22 1207	. 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  28947  axpasch  28957  exatleN  39407  ps-2b  39485  3atlem1  39486  3atlem2  39487  3atlem4  39489  3atlem5  39490  3atlem6  39491  2llnjaN  39569  4atlem12b  39614  2lplnja  39622  dalemqea  39630  dath2  39740  lneq2at  39781  llnexchb2  39872  dalawlem1  39874  lhpexle3lem  40014  cdleme26ee  40363  cdlemg34  40715  cdlemg35  40716  cdlemg36  40717  cdlemj1  40824  cdlemj2  40825  cdlemk23-3  40905  cdlemk25-3  40907  cdlemk26b-3  40908  cdlemk26-3  40909  cdleml3N  40981  iscnrm3llem2  48854