Theorem simp131 1306

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

Assertion

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

Proof of Theorem simp131

Step	Hyp	Ref	Expression
1		simp31 1207	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑)
2	1	3ad2ant1 1131	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1085

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 401  df-3an 1087

This theorem is referenced by:  ax5seglem3  26817  exatleN  36973  3atlem1  37052  3atlem2  37053  3atlem5  37056  2llnjaN  37135  4atlem11b  37177  4atlem12b  37180  lplncvrlvol2  37184  dalemsea  37198  dath2  37306  cdlemblem  37362  dalawlem1  37440  lhpexle3lem  37580  4atexlemex6  37643  cdleme22f2  37916  cdleme22g  37917  cdlemg7aN  38194  cdlemg34  38281  cdlemj1  38390  cdlemk23-3  38471  cdlemk25-3  38473  cdlemk26b-3  38474  cdleml3N  38547