Theorem simp123 1303

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

Assertion

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

Proof of Theorem simp123

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ax5seglem3  26716  axpasch  26726  exatleN  36539  ps-2b  36617  3atlem1  36618  3atlem2  36619  3atlem4  36621  3atlem5  36622  3atlem6  36623  2llnjaN  36701  2llnjN  36702  4atlem12b  36746  2lplnja  36754  2lplnj  36755  dalemrea  36763  dath2  36872  lneq2at  36913  osumcllem7N  37097  cdleme26ee  37495  cdlemg35  37848  cdlemg36  37849  cdlemj1  37956  cdlemk23-3  38037  cdlemk25-3  38039  cdlemk26b-3  38040  cdlemk27-3  38042  cdlemk28-3  38043  cdleml3N  38113