![]() |
Mathbox for Jonathan Ben-Naim |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bnj593 | Structured version Visualization version GIF version |
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
Ref | Expression |
---|---|
bnj593.1 | ⊢ (𝜑 → ∃𝑥𝜓) |
bnj593.2 | ⊢ (𝜓 → 𝜒) |
Ref | Expression |
---|---|
bnj593 | ⊢ (𝜑 → ∃𝑥𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj593.1 | . 2 ⊢ (𝜑 → ∃𝑥𝜓) | |
2 | bnj593.2 | . . 3 ⊢ (𝜓 → 𝜒) | |
3 | 2 | eximi 1909 | . 2 ⊢ (∃𝑥𝜓 → ∃𝑥𝜒) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝜑 → ∃𝑥𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1851 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 |
This theorem depends on definitions: df-bi 197 df-ex 1852 |
This theorem is referenced by: bnj1266 31187 bnj1304 31195 bnj1379 31206 bnj594 31287 bnj852 31296 bnj908 31306 bnj996 31330 bnj907 31340 bnj1128 31363 bnj1148 31369 bnj1154 31372 bnj1189 31382 bnj1245 31387 bnj1279 31391 bnj1286 31392 bnj1311 31397 bnj1371 31402 bnj1398 31407 bnj1408 31409 bnj1450 31423 bnj1498 31434 bnj1514 31436 bnj1501 31440 |
Copyright terms: Public domain | W3C validator |