![]() |
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 2176. See exlimiv 1908 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 2176 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) |
3 | exlimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 2, 3 | mpgbi 1780 | 1 ⊢ (∃𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1761 Ⅎwnf 1765 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-12 2141 |
This theorem depends on definitions: df-bi 208 df-ex 1762 df-nf 1766 |
This theorem is referenced by: exlimih 2263 equs5aALT 2341 equs5eALT 2342 equsex 2396 exdistrf 2426 equs5a 2437 equs5e 2438 dfmoeu 2572 moanim 2673 euan 2674 moexexlem 2681 2eu6 2714 ceqsex 3483 sbhypf 3495 vtoclgf 3508 vtoclg1f 3509 vtoclef 3526 rspn0 4233 reusv2lem1 5190 copsexg 5273 copsex2g 5275 rexopabb 5305 0nelopab 5340 ralxpf 5603 dmcoss 5723 fv3 6556 opabiota 6613 zfregcl 8904 scottex 9160 scott0 9161 dfac5lem5 9399 zfcndpow 9884 zfcndreg 9885 zfcndinf 9886 reclem2pr 10316 mreiincl 16696 brabgaf 30049 cnvoprabOLD 30144 bnj607 31804 bnj900 31817 exisym1 33381 exlimii 33724 bj-exlimmpi 33799 bj-exlimmpbi 33800 bj-exlimmpbir 33801 dihglblem5 37965 eu2ndop1stv 42840 |
Copyright terms: Public domain | W3C validator |