Theorem simp122 1307

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

Assertion

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

Proof of Theorem simp122

Step	Hyp	Ref	Expression
1		simp22 1208	. 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  4atlem12b  39593  2lplnja  39601  dalemqea  39609  dath2  39719  lneq2at  39760  llnexchb2  39851  dalawlem1  39853  lhpexle3lem  39993  cdleme26ee  40342  cdlemg34  40694  cdlemg35  40695  cdlemg36  40696  cdlemj1  40803  cdlemj2  40804  cdlemk23-3  40884  cdlemk25-3  40886  cdlemk26b-3  40887  cdlemk26-3  40888  cdleml3N  40960  iscnrm3llem2  48938