|   | 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 2206 and 19.21v 1938. (Contributed by NM, 31-Jul-1995.) | 
| Ref | Expression | 
|---|---|
| alrimivv.1 | ⊢ (𝜑 → 𝜓) | 
| Ref | Expression | 
|---|---|
| alrimivv | ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | alrimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 2 | 1 | alrimiv 1926 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) | 
| 3 | 2 | alrimiv 1926 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∀wal 1537 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1794 ax-4 1808 ax-5 1909 | 
| This theorem is referenced by: 2ax5 1936 2mo 2647 euind 3729 sbnfc2 4438 uniintsn 4984 eusvnf 5391 copsex2dv 5498 ssopab2dv 5555 ssrel 5791 ssrelOLD 5792 relssdv 5797 eqrelrdv 5801 eqbrrdv 5802 eqrelrdv2 5804 ssrelrel 5805 iss 6052 iresn0n0 6071 ordelord 6405 suctr 6469 funssres 6609 funun 6611 fununi 6640 fsn 7154 opabresex2d 7487 fvmptopabOLD 7489 ovg 7599 wemoiso 7999 wemoiso2 8000 oprabexd 8001 frrlem9 8320 omeu 8624 qliftfund 8844 eroveu 8853 fpwwe2lem10 10681 addsrmo 11114 mulsrmo 11115 seqf1o 14085 fi1uzind 14547 brfi1indALT 14550 summo 15754 prodmo 15973 pceu 16885 invfun 17809 initoeu2lem2 18061 psss 18626 psgneu 19525 gsumval3eu 19923 hausflimi 23989 vitalilem3 25646 plyexmo 26356 nosupprefixmo 27746 noinfprefixmo 27747 nosupno 27749 noinfno 27764 tglineintmo 28651 frgr3vlem1 30293 3vfriswmgrlem 30297 frgr2wwlk1 30349 pjhthmo 31322 chscl 31661 bnj1379 34845 bnj580 34928 bnj1321 35042 acycgr1v 35155 cvmlift2lem12 35320 satffunlem1lem1 35408 satffunlem2lem1 35410 mclsssvlem 35568 mclsax 35575 mclsind 35576 lineintmo 36159 trer 36318 mbfresfi 37674 unirep 37722 iss2 38346 prter1 38881 islpoldN 41487 ismrcd2 42715 ismrc 42717 tfsconcatb0 43362 mnutrd 44304 truniALT 44566 gen12 44643 sspwtrALT 44847 sspwtrALT2 44848 suctrALT 44851 suctrALT2 44862 trintALT 44906 suctrALTcf 44947 suctrALT3 44949 rlimdmafv 47194 rlimdmafv2 47275 opabresex0d 47302 spr0nelg 47468 sprsymrelfvlem 47482 mofsn 48758 thincmo 49102 functhincfun 49123 | 
| Copyright terms: Public domain | W3C validator |