Theorem simp121 1389

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

Assertion

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

Proof of Theorem simp121

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

Syntax hints:   → wi 4   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  ax5seglem3  26033  axpasch  26043  exatleN  35213  ps-2b  35291  3atlem1  35292  3atlem2  35293  3atlem4  35295  3atlem5  35296  3atlem6  35297  2llnjaN  35375  4atlem12b  35420  2lplnja  35428  dalempea  35435  dath2  35546  lneq2at  35587  llnexchb2  35678  dalawlem1  35680  osumcllem7N  35771  lhpexle3lem  35820  cdleme26ee  36170  cdlemg34  36522  cdlemg36  36524  cdlemj1  36631  cdlemj2  36632  cdlemk23-3  36712  cdlemk25-3  36714  cdlemk26b-3  36715  cdlemk26-3  36716  cdlemk27-3  36717  cdleml3N  36788