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 13879 fi1uzind 14325 brfi1indALT 14328 summo 15538 prodmo 15755 pceu 16654 invfun 17583 initoeu2lem2 17837 psss 18405 psgneu 19223 gsumval3eu 19616 hausflimi 23259 vitalilem3 24902 plyexmo 25601 nosupprefixmo 26976 noinfprefixmo 26977 nosupno 26979 noinfno 26994 tglineintmo 27389 frgr3vlem1 29022 3vfriswmgrlem 29026 frgr2wwlk1 29078 pjhthmo 30049 chscl 30388 bnj1379 33222 bnj580 33305 bnj1321 33419 acycgr1v 33523 cvmlift2lem12 33688 satffunlem1lem1 33776 satffunlem2lem1 33778 mclsssvlem 33936 mclsax 33943 mclsind 33944 lineintmo 34673 trer 34719 mbfresfi 36055 unirep 36103 iss2 36736 prter1 37272 islpoldN 39878 ismrcd2 40924 ismrc 40926 mnutrd 42361 truniALT 42624 gen12 42701 sspwtrALT 42905 sspwtrALT2 42906 suctrALT 42909 suctrALT2 42920 trintALT 42964 suctrALTcf 43005 suctrALT3 43007 rlimdmafv 45200 rlimdmafv2 45281 opabresex0d 45308 spr0nelg 45459 sprsymrelfvlem 45473 mofsn 46701 thincmo 46840 |
Copyright terms: Public domain | W3C validator |