Theorem simp123 1363

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

Assertion

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

Proof of Theorem simp123

Step	Hyp	Ref	Expression
1		simp23 1222	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜒)
2	1	3ad2ant1 1124	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  ax5seglem3  26280  axpasch  26290  exatleN  35552  ps-2b  35630  3atlem1  35631  3atlem2  35632  3atlem4  35634  3atlem5  35635  3atlem6  35636  2llnjaN  35714  2llnjN  35715  4atlem12b  35759  2lplnja  35767  2lplnj  35768  dalemrea  35776  dath2  35885  lneq2at  35926  osumcllem7N  36110  cdleme26ee  36508  cdlemg35  36861  cdlemg36  36862  cdlemj1  36969  cdlemk23-3  37050  cdlemk25-3  37052  cdlemk26b-3  37053  cdlemk27-3  37055  cdlemk28-3  37056  cdleml3N  37126