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 1135	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1089

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

This theorem is referenced by:  ax5seglem3  27022  axpasch  27032  exatleN  37155  ps-2b  37233  3atlem1  37234  3atlem2  37235  3atlem4  37237  3atlem5  37238  3atlem6  37239  2llnjaN  37317  4atlem12b  37362  2lplnja  37370  dalempea  37377  dath2  37488  lneq2at  37529  llnexchb2  37620  dalawlem1  37622  osumcllem7N  37713  lhpexle3lem  37762  cdleme26ee  38111  cdlemg34  38463  cdlemg36  38465  cdlemj1  38572  cdlemj2  38573  cdlemk23-3  38653  cdlemk25-3  38655  cdlemk26b-3  38656  cdlemk26-3  38657  cdlemk27-3  38658  cdleml3N  38729  iscnrm3llem2  45917