| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > exlimi | Structured version Visualization version GIF version | ||
| Description: Inference associated with 19.23 2211. See exlimiv 1930 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
| Ref | Expression |
|---|---|
| exlimi.1 | ⊢ Ⅎ𝑥𝜓 |
| exlimi.2 | ⊢ (𝜑 → 𝜓) |
| Ref | Expression |
|---|---|
| exlimi | ⊢ (∃𝑥𝜑 → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exlimi.1 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
| 2 | 1 | 19.23 2211 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) |
| 3 | exlimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
| 4 | 2, 3 | mpgbi 1798 | 1 ⊢ (∃𝑥𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∃wex 1779 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: sbalexOLD 2243 equsexv 2268 equs5av 2277 exlimih 2289 equs5aALT 2369 equs5eALT 2370 equsex 2423 exdistrf 2452 equs5a 2462 equs5e 2463 dfmoeu 2536 moanim 2620 euan 2621 moexexlem 2626 2eu6 2657 ceqsexOLD 3531 sbhypfOLD 3545 vtoclef 3563 vtoclgf 3569 vtoclg1f 3570 reusv2lem1 5398 copsexgw 5495 copsexg 5496 rexopabb 5533 ralxpf 5857 dmcoss 5985 fv3 6924 opabiota 6991 oprabidw 7462 zfregcl 9634 scottex 9925 scott0 9926 dfac5lem5 10167 zfcndpow 10656 zfcndreg 10657 zfcndinf 10658 reclem2pr 11088 mreiincl 17639 brabgaf 32620 bnj607 34930 bnj900 34943 exisym1 36425 exlimii 36832 bj-exlimmpi 36913 bj-exlimmpbi 36914 bj-exlimmpbir 36915 dihglblem5 41300 tworepnotupword 46901 eu2ndop1stv 47137 pgind 49236 |
| Copyright terms: Public domain | W3C validator |