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 1938 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 1806 | 1 ⊢ (∃𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1787 Ⅎwnf 1791 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-12 2177 |
This theorem depends on definitions: df-bi 210 df-ex 1788 df-nf 1792 |
This theorem is referenced by: sbalex 2242 equs5av 2277 exlimih 2292 equs5aALT 2365 equs5eALT 2366 equsex 2417 exdistrf 2446 equs5a 2456 equs5e 2457 dfmoeu 2535 moanim 2621 euan 2622 moexexlem 2627 2eu6 2657 ceqsex 3444 sbhypf 3457 vtoclgf 3469 vtoclg1f 3470 vtoclef 3489 rspn0OLD 4254 reusv2lem1 5276 copsexgw 5358 copsexg 5359 copsex2gOLD 5362 rexopabb 5394 0nelopabOLD 5432 ralxpf 5700 dmcoss 5825 fv3 6713 opabiota 6772 oprabidw 7222 zfregcl 9188 scottex 9466 scott0 9467 dfac5lem5 9706 zfcndpow 10195 zfcndreg 10196 zfcndinf 10197 reclem2pr 10627 mreiincl 17053 brabgaf 30621 cnvoprabOLD 30729 bnj607 32563 bnj900 32576 exisym1 34299 exlimii 34700 bj-exlimmpi 34784 bj-exlimmpbi 34785 bj-exlimmpbir 34786 dihglblem5 38998 eu2ndop1stv 44232 |
Copyright terms: Public domain | W3C validator |