Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > exlimiiv | Structured version Visualization version Unicode version |
Description: Inference associated with exlimiv 1858. (Contributed by BJ, 19-Dec-2020.) |
Ref | Expression |
---|---|
exlimiv.1 | |
exlimiiv.2 |
Ref | Expression |
---|---|
exlimiiv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimiiv.2 | . 2 | |
2 | exlimiv.1 | . . 3 | |
3 | 2 | exlimiv 1858 | . 2 |
4 | 1, 3 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-ex 1705 |
This theorem is referenced by: equid 1939 ax7 1943 ax12v2 2049 ax12vOLD 2050 ax12vOLDOLD 2051 19.8a 2052 ax6e 2250 axc11n 2307 axc11nOLD 2308 axc11nOLDOLD 2309 axc11nALT 2310 axext3 2604 bm1.3ii 4784 inf3 8532 epfrs 8607 kmlem2 8973 axcc2lem 9258 dcomex 9269 axdclem2 9342 grothpw 9648 grothpwex 9649 grothomex 9651 grothac 9652 cnso 14976 aannenlem3 24085 bj-ax6e 32653 wl-spae 33306 |
Copyright terms: Public domain | W3C validator |