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

This theorem is referenced by:  ax5seglem3  27202  exatleN  37345  3atlem1  37424  3atlem2  37425  3atlem5  37428  2llnjaN  37507  4atlem11b  37549  4atlem12b  37552  lplncvrlvol2  37556  dalemsea  37570  dath2  37678  cdlemblem  37734  dalawlem1  37812  lhpexle3lem  37952  4atexlemex6  38015  cdleme22f2  38288  cdleme22g  38289  cdlemg7aN  38566  cdlemg34  38653  cdlemj1  38762  cdlemk23-3  38843  cdlemk25-3  38845  cdlemk26b-3  38846  cdleml3N  38919