Theorem simp121 1305

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

Assertion

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

Proof of Theorem simp121

Step	Hyp	Ref	Expression
1		simp21 1206	. 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  28947  axpasch  28957  exatleN  39407  ps-2b  39485  3atlem1  39486  3atlem2  39487  3atlem4  39489  3atlem5  39490  3atlem6  39491  2llnjaN  39569  4atlem12b  39614  2lplnja  39622  dalempea  39629  dath2  39740  lneq2at  39781  llnexchb2  39872  dalawlem1  39874  osumcllem7N  39965  lhpexle3lem  40014  cdleme26ee  40363  cdlemg34  40715  cdlemg36  40717  cdlemj1  40824  cdlemj2  40825  cdlemk23-3  40905  cdlemk25-3  40907  cdlemk26b-3  40908  cdlemk26-3  40909  cdlemk27-3  40910  cdleml3N  40981  iscnrm3llem2  48854