Theorem simp132 1310

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

Assertion

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

Proof of Theorem simp132

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  ax5seglem3  28169  3atlem1  38292  3atlem2  38293  3atlem5  38296  2llnjaN  38375  4atlem11b  38417  4atlem12b  38420  lplncvrlvol2  38424  dalemtea  38439  dath2  38546  cdlemblem  38602  dalawlem1  38680  lhpexle3lem  38820  4atexlemex6  38883  cdleme22f2  39156  cdleme22g  39157  cdlemg7aN  39434  cdlemg34  39521  cdlemj1  39630  cdlemk23-3  39711  cdlemk25-3  39713  cdlemk26b-3  39714