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  28834  axpasch  28844  exatleN  39371  ps-2b  39449  3atlem1  39450  3atlem2  39451  3atlem4  39453  3atlem5  39454  3atlem6  39455  2llnjaN  39533  4atlem12b  39578  2lplnja  39586  dalemqea  39594  dath2  39704  lneq2at  39745  llnexchb2  39836  dalawlem1  39838  lhpexle3lem  39978  cdleme26ee  40327  cdlemg34  40679  cdlemg35  40680  cdlemg36  40681  cdlemj1  40788  cdlemj2  40789  cdlemk23-3  40869  cdlemk25-3  40871  cdlemk26b-3  40872  cdlemk26-3  40873  cdleml3N  40945  iscnrm3llem2  48911