![]() |
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 2136 and 19.21v 1898. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimivv | ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | alrimiv 1886 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1886 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1505 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1758 ax-4 1772 ax-5 1869 |
This theorem is referenced by: 2ax5 1896 2mo 2679 euind 3627 sbnfc2 4272 uniintsn 4786 eusvnf 5146 ssopab2dv 5290 ssrel 5507 relssdv 5511 eqrelrdv 5515 eqbrrdv 5516 eqrelrdv2 5518 ssrelrel 5519 iss 5748 ordelord 6051 suctr 6112 funssres 6231 funun 6233 fununi 6262 fsn 6720 opabresex2d 7027 fvmptopab 7028 ovg 7129 wemoiso 7486 wemoiso2 7487 oprabexd 7488 omeu 8012 qliftfund 8183 eroveu 8192 fpwwe2lem11 9860 addsrmo 10293 mulsrmo 10294 seqf1o 13226 fi1uzind 13666 brfi1indALT 13669 summo 14934 prodmo 15150 pceu 16039 invfun 16892 initoeu2lem2 17133 psss 17682 psgneu 18396 gsumval3eu 18778 hausflimi 22292 vitalilem3 23914 plyexmo 24605 tglineintmo 26130 frgr3vlem1 27807 3vfriswmgrlem 27811 frgr2wwlk1 27863 pjhthmo 28860 chscl 29199 bnj1379 31756 bnj580 31838 bnj1321 31950 cvmlift2lem12 32152 mclsssvlem 32335 mclsax 32342 mclsind 32343 frrlem9 32658 noprefixmo 32729 nosupno 32730 lineintmo 33145 trer 33191 mbfresfi 34385 unirep 34436 iss2 35053 prter1 35466 islpoldN 38071 ismrcd2 38697 ismrc 38699 mnutrd 39997 truniALT 40300 gen12 40377 sspwtrALT 40581 sspwtrALT2 40582 suctrALT 40585 suctrALT2 40596 trintALT 40640 suctrALTcf 40681 suctrALT3 40683 rlimdmafv 42788 rlimdmafv2 42869 opabresex0d 42896 spr0nelg 43012 sprsymrelfvlem 43026 |
Copyright terms: Public domain | W3C validator |