Theorem simp131 1304

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

Assertion

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

Proof of Theorem simp131

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ax5seglem3  26720  exatleN  36544  3atlem1  36623  3atlem2  36624  3atlem5  36627  2llnjaN  36706  4atlem11b  36748  4atlem12b  36751  lplncvrlvol2  36755  dalemsea  36769  dath2  36877  cdlemblem  36933  dalawlem1  37011  lhpexle3lem  37151  4atexlemex6  37214  cdleme22f2  37487  cdleme22g  37488  cdlemg7aN  37765  cdlemg34  37852  cdlemj1  37961  cdlemk23-3  38042  cdlemk25-3  38044  cdlemk26b-3  38045  cdleml3N  38118