Theorem simp132 1322

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

Assertion

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

Proof of Theorem simp132

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 1099

This theorem is referenced by:  ax5seglem3  29078  3atlem1  40071  3atlem2  40072  3atlem5  40075  2llnjaN  40154  4atlem11b  40196  4atlem12b  40199  lplncvrlvol2  40203  dalemtea  40218  dath2  40325  cdlemblem  40381  dalawlem1  40459  lhpexle3lem  40599  4atexlemex6  40662  cdleme22f2  40935  cdleme22g  40936  cdlemg7aN  41213  cdlemg34  41300  cdlemj1  41409  cdlemk23-3  41490  cdlemk25-3  41492  cdlemk26b-3  41493