![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > exlimi | Unicode version |
Description: Inference associated with 19.23 1910. See exlimiv 1722 for a version with a dv 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 1910 | . 2 |
3 | exlimi.2 | . 2 | |
4 | 2, 3 | mpgbi 1621 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 E. wex 1612
F/ wnf 1616 |
This theorem is referenced by: exlimih 1913 equs5a 1978 equs5e 1979 equsex 2038 nfeqf2 2041 exdistrf 2075 mo2v 2289 mo2vOLD 2290 mo2vOLDOLD 2291 moanim 2350 euan 2351 moexex 2363 2eu6 2383 ceqsex 3145 sbhypf 3156 vtoclgf 3165 vtoclg1f 3166 vtoclef 3182 rspn0 3797 reusv2lem1 4653 copsexg 4737 copsexgOLD 4738 copsex2g 4740 ralxpf 5154 dmcoss 5267 fv3 5884 tz6.12c 5890 opabiota 5936 0neqopab 6341 zfregcl 8041 scottex 8324 scott0 8325 dfac5lem5 8529 zfcndpow 9015 zfcndreg 9016 zfcndinf 9017 reclem2pr 9447 uzindOLD 10982 mreiincl 14993 cnvoprab 27546 exisym1 29889 eu2ndop1stv 32207 bnj607 33974 bnj900 33987 bj-equsexv 34312 exlimii 34404 bj-exlimmpi 34477 bj-exlimmpbi 34478 bj-exlimmpbir 34479 dihglblem5 37025 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-10 1837 ax-12 1854 |
This theorem depends on definitions: df-bi 185 df-ex 1613 df-nf 1617 |
Copyright terms: Public domain | W3C validator |