Theorem simp123 1308

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

Assertion

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

Proof of Theorem simp123

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  ax5seglem3  28894  axpasch  28904  exatleN  39386  ps-2b  39464  3atlem1  39465  3atlem2  39466  3atlem4  39468  3atlem5  39469  3atlem6  39470  2llnjaN  39548  2llnjN  39549  4atlem12b  39593  2lplnja  39601  2lplnj  39602  dalemrea  39610  dath2  39719  lneq2at  39760  osumcllem7N  39944  cdleme26ee  40342  cdlemg35  40695  cdlemg36  40696  cdlemj1  40803  cdlemk23-3  40884  cdlemk25-3  40886  cdlemk26b-3  40887  cdlemk27-3  40889  cdlemk28-3  40890  cdleml3N  40960  iscnrm3llem2  48938