Theorem simp121 1324

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

Assertion

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

Proof of Theorem simp121

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ax5seglem3  29542  axpasch  29552  exatleN  40664  ps-2b  40742  3atlem1  40743  3atlem2  40744  3atlem4  40746  3atlem5  40747  3atlem6  40748  2llnjaN  40826  4atlem12b  40871  2lplnja  40879  dalempea  40886  dath2  40997  lneq2at  41038  llnexchb2  41129  dalawlem1  41131  osumcllem7N  41222  lhpexle3lem  41271  cdleme26ee  41620  cdlemg34  41972  cdlemg36  41974  cdlemj1  42081  cdlemj2  42082  cdlemk23-3  42162  cdlemk25-3  42164  cdlemk26b-3  42165  cdlemk26-3  42166  cdlemk27-3  42167  cdleml3N  42238  iscnrm3llem2  50279