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

This theorem is referenced by:  ax5seglem3  26725  axpasch  26735  exatleN  36700  ps-2b  36778  3atlem1  36779  3atlem2  36780  3atlem4  36782  3atlem5  36783  3atlem6  36784  2llnjaN  36862  4atlem12b  36907  2lplnja  36915  dalempea  36922  dath2  37033  lneq2at  37074  llnexchb2  37165  dalawlem1  37167  osumcllem7N  37258  lhpexle3lem  37307  cdleme26ee  37656  cdlemg34  38008  cdlemg36  38010  cdlemj1  38117  cdlemj2  38118  cdlemk23-3  38198  cdlemk25-3  38200  cdlemk26b-3  38201  cdlemk26-3  38202  cdlemk27-3  38203  cdleml3N  38274