![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > eximd | Unicode version |
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
eximd.1 |
![]() ![]() ![]() ![]() |
eximd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eximd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximd.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | nfri 1774 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | eximd.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | eximdh 1595 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem is referenced by: exlimd 1820 19.41 1896 19.41OLD 1897 exdistrf 2028 sbied 2085 mo 2276 mopick2 2321 2euex 2326 copsexg 4402 ssopab2 4440 axextnd 8422 axpowndlem3 8430 axregndlem1 8433 axregnd 8435 finminlem 26211 ssrexf 27551 stoweidlem27 27643 stoweidlem34 27650 stoweidlem35 27651 exdistrfNEW7 29211 sbiedNEW7 29244 pmapglb2xN 30254 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-11 1757 |
This theorem depends on definitions: df-bi 178 df-ex 1548 df-nf 1551 |
Copyright terms: Public domain | W3C validator |