![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eximii | Structured version Visualization version Unicode version |
Description: Inference associated with eximi 1707. (Contributed by BJ, 3-Feb-2018.) |
Ref | Expression |
---|---|
eximii.1 |
![]() ![]() ![]() ![]() |
eximii.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eximii |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximii.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | eximii.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | eximi 1707 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | ax-mp 5 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 |
This theorem depends on definitions: df-bi 189 df-ex 1664 |
This theorem is referenced by: exiftru 1808 spimeh 1841 equidOLD 1856 ax6evr 1859 spimv1 2058 cbv3hvOLD 2062 cbv3hvOLDOLD 2063 ax6e 2094 spim 2098 spimed 2099 spimv 2101 spei 2105 equvini 2179 equveli 2180 euequ1 2305 euex 2323 darii 2394 barbari 2396 festino 2400 baroco 2401 cesaro 2402 camestros 2403 datisi 2404 disamis 2405 felapton 2408 darapti 2409 dimatis 2411 fresison 2412 calemos 2413 fesapo 2414 bamalip 2415 vtoclf 3099 vtocl 3100 axrep2 4517 axnul 4532 nalset 4540 notzfaus 4578 el 4585 dtru 4594 eusv2nf 4601 dvdemo1 4635 dvdemo2 4636 axpr 4638 snnex 6597 inf1 8127 bnd 8363 axpowndlem2 9023 grothomex 9254 bnj101 29529 axextdfeq 30444 ax8dfeq 30445 axextndbi 30451 snelsingles 30689 bj-ax6elem2 31265 bj-spimedv 31320 bj-spimvv 31322 bj-speiv 31325 bj-axrep2 31404 bj-nalset 31409 bj-el 31411 bj-dtru 31412 bj-dvdemo1 31417 bj-dvdemo2 31418 ax6er 31435 bj-vtoclf 31515 wl-exeq 31867 eximp-surprise2 40577 |
Copyright terms: Public domain | W3C validator |