Theorem simp121 1301

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

Assertion

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

Proof of Theorem simp121

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ax5seglem3  26717  axpasch  26727  exatleN  36555  ps-2b  36633  3atlem1  36634  3atlem2  36635  3atlem4  36637  3atlem5  36638  3atlem6  36639  2llnjaN  36717  4atlem12b  36762  2lplnja  36770  dalempea  36777  dath2  36888  lneq2at  36929  llnexchb2  37020  dalawlem1  37022  osumcllem7N  37113  lhpexle3lem  37162  cdleme26ee  37511  cdlemg34  37863  cdlemg36  37865  cdlemj1  37972  cdlemj2  37973  cdlemk23-3  38053  cdlemk25-3  38055  cdlemk26b-3  38056  cdlemk26-3  38057  cdlemk27-3  38058  cdleml3N  38129