Theorem simp121 1307

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

Assertion

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

Proof of Theorem simp121

Step	Hyp	Ref	Expression
1		simp21 1208	. 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  4atlem12b  40057  2lplnja  40065  dalempea  40072  dath2  40183  lneq2at  40224  llnexchb2  40315  dalawlem1  40317  osumcllem7N  40408  lhpexle3lem  40457  cdleme26ee  40806  cdlemg34  41158  cdlemg36  41160  cdlemj1  41267  cdlemj2  41268  cdlemk23-3  41348  cdlemk25-3  41350  cdlemk26b-3  41351  cdlemk26-3  41352  cdlemk27-3  41353  cdleml3N  41424  iscnrm3llem2  49425