![]() |
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 2199. See exlimiv 1925 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 2199 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) |
3 | exlimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 2, 3 | mpgbi 1792 | 1 ⊢ (∃𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1773 Ⅎwnf 1777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-ex 1774 df-nf 1778 |
This theorem is referenced by: sbalex 2230 equsexv 2254 equs5av 2265 exlimih 2278 equs5aALT 2357 equs5eALT 2358 equsex 2411 exdistrf 2440 equs5a 2450 equs5e 2451 dfmoeu 2524 moanim 2608 euan 2609 moexexlem 2614 2eu6 2645 ceqsexOLD 3513 sbhypfOLD 3529 vtoclef 3541 vtoclgf 3548 vtoclg1f 3549 rspn0OLD 4353 reusv2lem1 5398 copsexgw 5492 copsexg 5493 copsex2gOLD 5496 rexopabb 5530 0nelopabOLD 5570 ralxpf 5849 dmcoss 5974 fv3 6914 opabiota 6980 oprabidw 7450 zfregcl 9619 scottex 9910 scott0 9911 dfac5lem5 10152 zfcndpow 10641 zfcndreg 10642 zfcndinf 10643 reclem2pr 11073 mreiincl 17579 brabgaf 32477 cnvoprabOLD 32584 bnj607 34678 bnj900 34691 exisym1 36039 exlimii 36439 bj-exlimmpi 36521 bj-exlimmpbi 36522 bj-exlimmpbir 36523 dihglblem5 40901 tworepnotupword 46410 eu2ndop1stv 46643 pgind 48334 |
Copyright terms: Public domain | W3C validator |