Theorem simp121 1302

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

Assertion

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

Proof of Theorem simp121

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 396  df-3an 1086

This theorem is referenced by:  ax5seglem3  28661  axpasch  28671  exatleN  38769  ps-2b  38847  3atlem1  38848  3atlem2  38849  3atlem4  38851  3atlem5  38852  3atlem6  38853  2llnjaN  38931  4atlem12b  38976  2lplnja  38984  dalempea  38991  dath2  39102  lneq2at  39143  llnexchb2  39234  dalawlem1  39236  osumcllem7N  39327  lhpexle3lem  39376  cdleme26ee  39725  cdlemg34  40077  cdlemg36  40079  cdlemj1  40186  cdlemj2  40187  cdlemk23-3  40267  cdlemk25-3  40269  cdlemk26b-3  40270  cdlemk26-3  40271  cdlemk27-3  40272  cdleml3N  40343  iscnrm3llem2  47795