Theorem simp121 1303

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

Assertion

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

Proof of Theorem simp121

Step	Hyp	Ref	Expression
1		simp21 1204	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜑)
2	1	3ad2ant1 1131	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  ax5seglem3  28456  axpasch  28466  exatleN  38578  ps-2b  38656  3atlem1  38657  3atlem2  38658  3atlem4  38660  3atlem5  38661  3atlem6  38662  2llnjaN  38740  4atlem12b  38785  2lplnja  38793  dalempea  38800  dath2  38911  lneq2at  38952  llnexchb2  39043  dalawlem1  39045  osumcllem7N  39136  lhpexle3lem  39185  cdleme26ee  39534  cdlemg34  39886  cdlemg36  39888  cdlemj1  39995  cdlemj2  39996  cdlemk23-3  40076  cdlemk25-3  40078  cdlemk26b-3  40079  cdlemk26-3  40080  cdlemk27-3  40081  cdleml3N  40152  iscnrm3llem2  47670