Theorem simp121 1304

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

Assertion

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

Proof of Theorem simp121

Step	Hyp	Ref	Expression
1		simp21 1205	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜑)
2	1	3ad2ant1 1132	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ax5seglem3  27308  axpasch  27318  exatleN  37425  ps-2b  37503  3atlem1  37504  3atlem2  37505  3atlem4  37507  3atlem5  37508  3atlem6  37509  2llnjaN  37587  4atlem12b  37632  2lplnja  37640  dalempea  37647  dath2  37758  lneq2at  37799  llnexchb2  37890  dalawlem1  37892  osumcllem7N  37983  lhpexle3lem  38032  cdleme26ee  38381  cdlemg34  38733  cdlemg36  38735  cdlemj1  38842  cdlemj2  38843  cdlemk23-3  38923  cdlemk25-3  38925  cdlemk26b-3  38926  cdlemk26-3  38927  cdlemk27-3  38928  cdleml3N  38999  iscnrm3llem2  46255