![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > alrimivv | Structured version Visualization version GIF version |
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2196 and 19.21v 1935. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimivv | ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | alrimiv 1923 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1923 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1532 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem is referenced by: 2ax5 1933 2mo 2637 euind 3718 sbnfc2 4441 uniintsn 4997 eusvnf 5398 ssopab2dv 5559 ssrel 5790 ssrelOLD 5791 relssdv 5796 eqrelrdv 5800 eqbrrdv 5801 eqrelrdv2 5803 ssrelrel 5804 iss 6046 iresn0n0 6065 ordelord 6400 suctr 6464 funssres 6605 funun 6607 fununi 6636 fsn 7151 opabresex2d 7480 fvmptopabOLD 7482 ovg 7593 wemoiso 7989 wemoiso2 7990 oprabexd 7991 frrlem9 8311 omeu 8617 qliftfund 8834 eroveu 8843 fpwwe2lem10 10685 addsrmo 11118 mulsrmo 11119 seqf1o 14065 fi1uzind 14518 brfi1indALT 14521 summo 15723 prodmo 15940 pceu 16850 invfun 17782 initoeu2lem2 18039 psss 18607 psgneu 19506 gsumval3eu 19904 hausflimi 23978 vitalilem3 25633 plyexmo 26344 nosupprefixmo 27733 noinfprefixmo 27734 nosupno 27736 noinfno 27751 tglineintmo 28572 frgr3vlem1 30209 3vfriswmgrlem 30213 frgr2wwlk1 30265 pjhthmo 31238 chscl 31577 copsex2dv 32528 bnj1379 34677 bnj580 34760 bnj1321 34874 acycgr1v 34979 cvmlift2lem12 35144 satffunlem1lem1 35232 satffunlem2lem1 35234 mclsssvlem 35392 mclsax 35399 mclsind 35400 lineintmo 35983 trer 36030 mbfresfi 37369 unirep 37417 iss2 38044 prter1 38579 islpoldN 41185 ismrcd2 42374 ismrc 42376 tfsconcatb0 43028 mnutrd 43972 truniALT 44235 gen12 44312 sspwtrALT 44516 sspwtrALT2 44517 suctrALT 44520 suctrALT2 44531 trintALT 44575 suctrALTcf 44616 suctrALT3 44618 rlimdmafv 46808 rlimdmafv2 46889 opabresex0d 46916 spr0nelg 47066 sprsymrelfvlem 47080 mofsn 48229 thincmo 48368 |
Copyright terms: Public domain | W3C validator |