![]() |
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 1910 | . 2 ⊢ (∃𝑥𝜓 → ∃𝑥𝜒) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝜑 → ∃𝑥𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1852 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 |
This theorem depends on definitions: df-bi 197 df-ex 1853 |
This theorem is referenced by: bnj1266 31220 bnj1304 31228 bnj1379 31239 bnj594 31320 bnj852 31329 bnj908 31339 bnj996 31363 bnj907 31373 bnj1128 31396 bnj1148 31402 bnj1154 31405 bnj1189 31415 bnj1245 31420 bnj1279 31424 bnj1286 31425 bnj1311 31430 bnj1371 31435 bnj1398 31440 bnj1408 31442 bnj1450 31456 bnj1498 31467 bnj1514 31469 bnj1501 31473 |
Copyright terms: Public domain | W3C validator |