Theorem simp121 1322

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

Assertion

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

Proof of Theorem simp121

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ax5seglem3  29186  axpasch  29196  exatleN  40035  ps-2b  40113  3atlem1  40114  3atlem2  40115  3atlem4  40117  3atlem5  40118  3atlem6  40119  2llnjaN  40197  4atlem12b  40242  2lplnja  40250  dalempea  40257  dath2  40368  lneq2at  40409  llnexchb2  40500  dalawlem1  40502  osumcllem7N  40593  lhpexle3lem  40642  cdleme26ee  40991  cdlemg34  41343  cdlemg36  41345  cdlemj1  41452  cdlemj2  41453  cdlemk23-3  41533  cdlemk25-3  41535  cdlemk26b-3  41536  cdlemk26-3  41537  cdlemk27-3  41538  cdleml3N  41609  iscnrm3llem2  49580