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  29502  axpasch  29512  exatleN  40441  ps-2b  40519  3atlem1  40520  3atlem2  40521  3atlem4  40523  3atlem5  40524  3atlem6  40525  2llnjaN  40603  2llnjN  40604  4atlem12b  40648  2lplnja  40656  2lplnj  40657  dalemrea  40665  dath2  40774  lneq2at  40815  osumcllem7N  40999  cdleme26ee  41397  cdlemg35  41750  cdlemg36  41751  cdlemj1  41858  cdlemk23-3  41939  cdlemk25-3  41941  cdlemk26b-3  41942  cdlemk27-3  41944  cdlemk28-3  41945  cdleml3N  42015  iscnrm3llem2  50027