Theorem simp131 1309

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

Assertion

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

Proof of Theorem simp131

Step	Hyp	Ref	Expression
1		simp31 1210	. 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  29004  exatleN  39664  3atlem1  39743  3atlem2  39744  3atlem5  39747  2llnjaN  39826  4atlem11b  39868  4atlem12b  39871  lplncvrlvol2  39875  dalemsea  39889  dath2  39997  cdlemblem  40053  dalawlem1  40131  lhpexle3lem  40271  4atexlemex6  40334  cdleme22f2  40607  cdleme22g  40608  cdlemg7aN  40885  cdlemg34  40972  cdlemj1  41081  cdlemk23-3  41162  cdlemk25-3  41164  cdlemk26b-3  41165  cdleml3N  41238