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 1762 | . 2 ⊢ (∃𝑥𝜓 → ∃𝑥𝜒) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝜑 → ∃𝑥𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ex 1705 |
This theorem is referenced by: bnj1266 30882 bnj1304 30890 bnj1379 30901 bnj594 30982 bnj852 30991 bnj908 31001 bnj996 31025 bnj907 31035 bnj1128 31058 bnj1148 31064 bnj1154 31067 bnj1189 31077 bnj1245 31082 bnj1279 31086 bnj1286 31087 bnj1311 31092 bnj1371 31097 bnj1398 31102 bnj1408 31104 bnj1450 31118 bnj1498 31129 bnj1514 31131 bnj1501 31135 |
Copyright terms: Public domain | W3C validator |