Theorem simp131 1315

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

Assertion

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

Proof of Theorem simp131

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ax5seglem3  29018  exatleN  39896  3atlem1  39975  3atlem2  39976  3atlem5  39979  2llnjaN  40058  4atlem11b  40100  4atlem12b  40103  lplncvrlvol2  40107  dalemsea  40121  dath2  40229  cdlemblem  40285  dalawlem1  40363  lhpexle3lem  40503  4atexlemex6  40566  cdleme22f2  40839  cdleme22g  40840  cdlemg7aN  41117  cdlemg34  41204  cdlemj1  41313  cdlemk23-3  41394  cdlemk25-3  41396  cdlemk26b-3  41397  cdleml3N  41470