Theorem simp123 1309

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

Assertion

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

Proof of Theorem simp123

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ax5seglem3  29000  axpasch  29010  exatleN  39850  ps-2b  39928  3atlem1  39929  3atlem2  39930  3atlem4  39932  3atlem5  39933  3atlem6  39934  2llnjaN  40012  2llnjN  40013  4atlem12b  40057  2lplnja  40065  2lplnj  40066  dalemrea  40074  dath2  40183  lneq2at  40224  osumcllem7N  40408  cdleme26ee  40806  cdlemg35  41159  cdlemg36  41160  cdlemj1  41267  cdlemk23-3  41348  cdlemk25-3  41350  cdlemk26b-3  41351  cdlemk27-3  41353  cdlemk28-3  41354  cdleml3N  41424  iscnrm3llem2  49425