Theorem simp132 1328

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

Assertion

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

Proof of Theorem simp132

Step	Hyp	Ref	Expression
1		simp32 1229	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓)
2	1	3ad2ant1 1151	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1103

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 1105

This theorem is referenced by:  ax5seglem3  29259  3atlem1  40235  3atlem2  40236  3atlem5  40239  2llnjaN  40318  4atlem11b  40360  4atlem12b  40363  lplncvrlvol2  40367  dalemtea  40382  dath2  40489  cdlemblem  40545  dalawlem1  40623  lhpexle3lem  40763  4atexlemex6  40826  cdleme22f2  41099  cdleme22g  41100  cdlemg7aN  41377  cdlemg34  41464  cdlemj1  41573  cdlemk23-3  41654  cdlemk25-3  41656  cdlemk26b-3  41657