![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp133 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp133 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp33 1253 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜒) | |
2 | 1 | 3ad2ant1 1127 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1071 |
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 197 df-an 383 df-3an 1073 |
This theorem is referenced by: tsmsxp 22178 ax5seglem3 26032 exatleN 35212 3atlem1 35291 3atlem2 35292 3atlem6 35296 4atlem11b 35416 4atlem12b 35419 lplncvrlvol2 35423 dalemuea 35439 dath2 35545 4atexlemex6 35882 cdleme22f2 36156 cdleme22g 36157 cdlemg7aN 36434 cdlemg31c 36508 cdlemg36 36523 cdlemj1 36630 cdlemj2 36631 cdlemk23-3 36711 cdlemk26b-3 36714 |
Copyright terms: Public domain | W3C validator |