Theorem simp121 1306

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

Assertion

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

Proof of Theorem simp121

Step	Hyp	Ref	Expression
1		simp21 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  28910  axpasch  28920  exatleN  39449  ps-2b  39527  3atlem1  39528  3atlem2  39529  3atlem4  39531  3atlem5  39532  3atlem6  39533  2llnjaN  39611  4atlem12b  39656  2lplnja  39664  dalempea  39671  dath2  39782  lneq2at  39823  llnexchb2  39914  dalawlem1  39916  osumcllem7N  40007  lhpexle3lem  40056  cdleme26ee  40405  cdlemg34  40757  cdlemg36  40759  cdlemj1  40866  cdlemj2  40867  cdlemk23-3  40947  cdlemk25-3  40949  cdlemk26b-3  40950  cdlemk26-3  40951  cdlemk27-3  40952  cdleml3N  41023  iscnrm3llem2  48987