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 2200 and 19.21v 1934. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimivv | ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | alrimiv 1922 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1922 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1529 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1790 ax-4 1804 ax-5 1905 |
This theorem is referenced by: 2ax5 1932 2mo 2727 euind 3713 sbnfc2 4386 uniintsn 4904 eusvnf 5283 ssopab2dv 5429 ssrel 5650 relssdv 5654 eqrelrdv 5658 eqbrrdv 5659 eqrelrdv2 5661 ssrelrel 5662 iss 5896 iresn0n0 5916 ordelord 6206 suctr 6267 funssres 6391 funun 6393 fununi 6422 fsn 6890 opabresex2d 7200 fvmptopab 7201 ovg 7305 wemoiso 7666 wemoiso2 7667 oprabexd 7668 omeu 8203 qliftfund 8375 eroveu 8384 fpwwe2lem11 10054 addsrmo 10487 mulsrmo 10488 seqf1o 13403 fi1uzind 13847 brfi1indALT 13850 summo 15066 prodmo 15282 pceu 16175 invfun 17026 initoeu2lem2 17267 psss 17816 psgneu 18626 gsumval3eu 19016 hausflimi 22580 vitalilem3 24203 plyexmo 24894 tglineintmo 26420 frgr3vlem1 28044 3vfriswmgrlem 28048 frgr2wwlk1 28100 pjhthmo 29071 chscl 29410 bnj1379 32095 bnj580 32178 bnj1321 32292 acycgr1v 32389 cvmlift2lem12 32554 satffunlem1lem1 32642 satffunlem2lem1 32644 mclsssvlem 32802 mclsax 32809 mclsind 32810 frrlem9 33124 noprefixmo 33195 nosupno 33196 lineintmo 33611 trer 33657 mbfresfi 34930 unirep 34980 iss2 35593 prter1 36007 islpoldN 38612 ismrcd2 39287 ismrc 39289 mnutrd 40607 truniALT 40866 gen12 40943 sspwtrALT 41147 sspwtrALT2 41148 suctrALT 41151 suctrALT2 41162 trintALT 41206 suctrALTcf 41247 suctrALT3 41249 rlimdmafv 43367 rlimdmafv2 43448 opabresex0d 43475 spr0nelg 43629 sprsymrelfvlem 43643 |
Copyright terms: Public domain | W3C validator |