Theorem simp121 1312

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

Assertion

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

Proof of Theorem simp121

Step	Hyp	Ref	Expression
1		simp21 1213	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜑)
2	1	3ad2ant1 1139	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ax5seglem3  29025  axpasch  29035  exatleN  39903  ps-2b  39981  3atlem1  39982  3atlem2  39983  3atlem4  39985  3atlem5  39986  3atlem6  39987  2llnjaN  40065  4atlem12b  40110  2lplnja  40118  dalempea  40125  dath2  40236  lneq2at  40277  llnexchb2  40368  dalawlem1  40370  osumcllem7N  40461  lhpexle3lem  40510  cdleme26ee  40859  cdlemg34  41211  cdlemg36  41213  cdlemj1  41320  cdlemj2  41321  cdlemk23-3  41401  cdlemk25-3  41403  cdlemk26b-3  41404  cdlemk26-3  41405  cdlemk27-3  41406  cdleml3N  41477  iscnrm3llem2  49447