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 2201 and 19.21v 1943. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimivv | ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | alrimiv 1931 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1931 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem is referenced by: 2ax5 1941 2mo 2650 euind 3681 sbnfc2 4395 uniintsn 4947 eusvnf 5346 ssopab2dv 5506 ssrel 5735 ssrelOLD 5736 relssdv 5741 eqrelrdv 5745 eqbrrdv 5746 eqrelrdv2 5748 ssrelrel 5749 iss 5986 iresn0n0 6004 ordelord 6336 suctr 6400 funssres 6541 funun 6543 fununi 6572 fsn 7076 opabresex2d 7403 fvmptopabOLD 7405 ovg 7512 wemoiso 7897 wemoiso2 7898 oprabexd 7899 frrlem9 8193 omeu 8500 qliftfund 8676 eroveu 8685 fpwwe2lem10 10510 addsrmo 10943 mulsrmo 10944 seqf1o 13878 fi1uzind 14324 brfi1indALT 14327 summo 15537 prodmo 15754 pceu 16653 invfun 17582 initoeu2lem2 17836 psss 18404 psgneu 19221 gsumval3eu 19611 hausflimi 23254 vitalilem3 24897 plyexmo 25596 nosupprefixmo 26971 noinfprefixmo 26972 nosupno 26974 noinfno 26989 tglineintmo 27383 frgr3vlem1 29016 3vfriswmgrlem 29020 frgr2wwlk1 29072 pjhthmo 30043 chscl 30382 bnj1379 33216 bnj580 33299 bnj1321 33413 acycgr1v 33517 cvmlift2lem12 33682 satffunlem1lem1 33770 satffunlem2lem1 33772 mclsssvlem 33930 mclsax 33937 mclsind 33938 lineintmo 34638 trer 34684 mbfresfi 36020 unirep 36068 iss2 36701 prter1 37237 islpoldN 39843 ismrcd2 40888 ismrc 40890 mnutrd 42325 truniALT 42588 gen12 42665 sspwtrALT 42869 sspwtrALT2 42870 suctrALT 42873 suctrALT2 42884 trintALT 42928 suctrALTcf 42969 suctrALT3 42971 rlimdmafv 45164 rlimdmafv2 45245 opabresex0d 45272 spr0nelg 45423 sprsymrelfvlem 45437 mofsn 46665 thincmo 46804 |
Copyright terms: Public domain | W3C validator |