Theorem simp121 1306

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

Assertion

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

Proof of Theorem simp121

Step	Hyp	Ref	Expression
1		simp21 1207	. 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  28913  axpasch  28923  exatleN  39526  ps-2b  39604  3atlem1  39605  3atlem2  39606  3atlem4  39608  3atlem5  39609  3atlem6  39610  2llnjaN  39688  4atlem12b  39733  2lplnja  39741  dalempea  39748  dath2  39859  lneq2at  39900  llnexchb2  39991  dalawlem1  39993  osumcllem7N  40084  lhpexle3lem  40133  cdleme26ee  40482  cdlemg34  40834  cdlemg36  40836  cdlemj1  40943  cdlemj2  40944  cdlemk23-3  41024  cdlemk25-3  41026  cdlemk26b-3  41027  cdlemk26-3  41028  cdlemk27-3  41029  cdleml3N  41100  iscnrm3llem2  49077