Theorem simp121 1405

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

Assertion

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

Proof of Theorem simp121

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

Syntax hints:   → wi 4   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  ax5seglem3  26168  axpasch  26178  exatleN  35425  ps-2b  35503  3atlem1  35504  3atlem2  35505  3atlem4  35507  3atlem5  35508  3atlem6  35509  2llnjaN  35587  4atlem12b  35632  2lplnja  35640  dalempea  35647  dath2  35758  lneq2at  35799  llnexchb2  35890  dalawlem1  35892  osumcllem7N  35983  lhpexle3lem  36032  cdleme26ee  36381  cdlemg34  36733  cdlemg36  36735  cdlemj1  36842  cdlemj2  36843  cdlemk23-3  36923  cdlemk25-3  36925  cdlemk26b-3  36926  cdlemk26-3  36927  cdlemk27-3  36928  cdleml3N  36999