Theorem simp121 1318

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

Assertion

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

Proof of Theorem simp121

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ax5seglem3  29088  axpasch  29098  exatleN  39988  ps-2b  40066  3atlem1  40067  3atlem2  40068  3atlem4  40070  3atlem5  40071  3atlem6  40072  2llnjaN  40150  4atlem12b  40195  2lplnja  40203  dalempea  40210  dath2  40321  lneq2at  40362  llnexchb2  40453  dalawlem1  40455  osumcllem7N  40546  lhpexle3lem  40595  cdleme26ee  40944  cdlemg34  41296  cdlemg36  41298  cdlemj1  41405  cdlemj2  41406  cdlemk23-3  41486  cdlemk25-3  41488  cdlemk26b-3  41489  cdlemk26-3  41490  cdlemk27-3  41491  cdleml3N  41562  iscnrm3llem2  49531