![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > aleximi | Structured version Visualization version Unicode version |
Description: A variant of al2imi 1698: instead of applying ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
aleximi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
aleximi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aleximi.1 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | con3d 140 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | al2imi 1698 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | alnex 1676 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | alnex 1676 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3imtr3g 277 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | con4d 109 |
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 1680 ax-4 1693 |
This theorem depends on definitions: df-bi 190 df-ex 1675 |
This theorem is referenced by: alexbii 1716 exim 1717 exbiOLD 1728 eximdh 1735 19.29 1746 19.29r 1747 19.35 1751 19.25 1754 19.30 1755 19.40b 1761 speimfw 1804 aev 2037 2ax6elem 2289 mo3 2347 mopick 2375 2mo 2391 eleq2dOLD 2526 ssopab2 4741 opabbrexOLD 6358 ssoprab2 6374 axextnd 9042 bj-2exim 31248 bj-exaleximi 31269 bj-sb56 31297 wl-mo3t 31950 pm10.56 36763 2exim 36772 |
Copyright terms: Public domain | W3C validator |