Theorem simp123 1326

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

Assertion

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

Proof of Theorem simp123

Step	Hyp	Ref	Expression
1		simp23 1227	. 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  29516  axpasch  29526  exatleN  40568  ps-2b  40646  3atlem1  40647  3atlem2  40648  3atlem4  40650  3atlem5  40651  3atlem6  40652  2llnjaN  40730  2llnjN  40731  4atlem12b  40775  2lplnja  40783  2lplnj  40784  dalemrea  40792  dath2  40901  lneq2at  40942  osumcllem7N  41126  cdleme26ee  41524  cdlemg35  41877  cdlemg36  41878  cdlemj1  41985  cdlemk23-3  42066  cdlemk25-3  42068  cdlemk26b-3  42069  cdlemk27-3  42071  cdlemk28-3  42072  cdleml3N  42142  iscnrm3llem2  50171