![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > alrimivv | Structured version Visualization version Unicode version |
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1992 and 19.21v 1790. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
alrimivv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | alrimiv 1777 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | alrimiv 1777 |
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-gen 1673 ax-4 1686 ax-5 1762 |
This theorem is referenced by: 2ax5 1788 2mo 2381 euind 3193 sbnfc2 3764 uniintsn 4242 eusvnf 4571 ssopab2dv 4703 ssrel 4901 relssdv 4905 eqrelrdv 4909 eqbrrdv 4910 eqrelrdv2 4912 ssrelrel 4913 iss 5130 ordelord 5424 suctr 5485 funssres 5601 funun 5603 fununi 5631 fsn 6046 ovg 6423 wemoiso 6766 wemoiso2 6767 oprabexd 6768 omeu 7273 qliftfund 7436 eroveu 7445 fpwwe2lem11 9052 addsrmo 9484 mulsrmo 9485 seqf1o 12248 fi1uzind 12645 brfi1indALT 12648 summo 13794 prodmo 14001 pceu 14807 invfun 15680 initoeu2lem2 15921 psss 16471 psgneu 17158 gsumval3eu 17549 hausflimi 21006 vitalilem3 22580 plyexmo 23278 tglineintmo 24699 frgra3vlem1 25740 3vfriswmgralem 25744 frg2wot1 25797 2spotdisj 25801 pjhthmo 26967 chscl 27306 bnj1379 29648 bnj580 29730 bnj1321 29842 cvmlift2lem12 30043 mclsssvlem 30206 mclsax 30213 mclsind 30214 lineintmo 30930 trer 30978 mbfresfi 31989 unirep 32041 prter1 32453 islpoldN 35054 ismrcd2 35543 ismrc 35545 truniALT 36903 gen12 36997 sspwtrALT 37207 sspwtrALT2 37216 suctrALT 37219 suctrALT2 37230 trintALT 37275 suctrALTcf 37316 suctrALT3 37318 rlimdmafv 38770 opabresex0d 39123 opabresex2d 39127 |
Copyright terms: Public domain | W3C validator |