Theorem simp131 1322

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

Assertion

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

Proof of Theorem simp131

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

Syntax hints:   → wi 4   ∧ w3a 1098

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 400  df-3an 1100

This theorem is referenced by:  ax5seglem3  29132  exatleN  40028  3atlem1  40107  3atlem2  40108  3atlem5  40111  2llnjaN  40190  4atlem11b  40232  4atlem12b  40235  lplncvrlvol2  40239  dalemsea  40253  dath2  40361  cdlemblem  40417  dalawlem1  40495  lhpexle3lem  40635  4atexlemex6  40698  cdleme22f2  40971  cdleme22g  40972  cdlemg7aN  41249  cdlemg34  41336  cdlemj1  41445  cdlemk23-3  41526  cdlemk25-3  41528  cdlemk26b-3  41529  cdleml3N  41602