|   | 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 1834 | . 2 ⊢ (∃𝑥𝜓 → ∃𝑥𝜒) | 
| 4 | 1, 3 | syl 17 | 1 ⊢ (𝜑 → ∃𝑥𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∃wex 1778 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-ex 1779 | 
| This theorem is referenced by: bnj1266 34826 bnj1304 34834 bnj1379 34845 bnj594 34927 bnj852 34936 bnj908 34946 bnj996 34971 bnj907 34982 bnj1128 35005 bnj1148 35011 bnj1154 35014 bnj1189 35024 bnj1245 35029 bnj1279 35033 bnj1286 35034 bnj1311 35039 bnj1371 35044 bnj1398 35049 bnj1408 35051 bnj1450 35065 bnj1498 35076 bnj1514 35078 bnj1501 35082 | 
| Copyright terms: Public domain | W3C validator |