![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > alrimdv | Unicode version |
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1905 and 19.21v 1729. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
alrimdv.1 |
Ref | Expression |
---|---|
alrimdv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1704 | . 2 | |
2 | ax-5 1704 | . 2 | |
3 | alrimdv.1 | . 2 | |
4 | 1, 2, 3 | alrimdh 1672 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 A. wal 1393 |
This theorem is referenced by: axc9lem2 2040 zfpair 4689 fliftfun 6210 isofrlem 6236 funcnvuni 6753 f1oweALT 6784 findcard 7779 findcard2 7780 dfac5lem4 8528 dfac5 8530 zorn2lem4 8900 genpcl 9407 psslinpr 9430 ltaddpr 9433 ltexprlem3 9437 suplem1pr 9451 uzwo 11173 uzwoOLD 11174 seqf1o 12148 ramcl 14547 alexsubALTlem3 20549 truniALT 33312 ggen31 33317 onfrALTlem2 33318 gen21 33405 gen22 33408 ggen22 33409 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1618 ax-4 1631 ax-5 1704 |
Copyright terms: Public domain | W3C validator |