![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 2eximdv | Structured version Unicode version |
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 3-Aug-1995.) |
Ref | Expression |
---|---|
2alimdv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2eximdv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2alimdv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eximdv 1677 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | eximdv 1677 |
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 1592 ax-4 1603 ax-5 1671 |
This theorem depends on definitions: df-bi 185 df-ex 1588 |
This theorem is referenced by: 2eu6 2380 cgsex2g 3112 cgsex4g 3113 spc2egv 3165 spc3egv 3167 relop 5099 elres 5254 th3q 7320 en3 7661 en4 7662 hash2prde 12298 pmtrrn2 16086 usgrarnedg 23456 fundmpss 27722 pellexlem5 29323 fnchoice 29900 stoweidlem35 29979 stoweidlem60 30004 hash2prv 30375 hash2sspr 30376 ax6e2eq 31599 |
Copyright terms: Public domain | W3C validator |