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 2075 and 19.21v 1868. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimivv | ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | alrimiv 1855 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1855 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1481 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem is referenced by: 2ax5 1866 2mo 2551 euind 3393 sbnfc2 4007 uniintsn 4514 eusvnf 4861 ssopab2dv 5004 ssrel 5207 ssrelOLD 5208 relssdv 5212 eqrelrdv 5216 eqbrrdv 5217 eqrelrdv2 5219 ssrelrel 5220 iss 5447 ordelord 5745 suctr 5808 suctrOLD 5809 funssres 5930 funun 5932 fununi 5964 fsn 6402 opabresex2d 6696 fvmptopab 6697 ovg 6799 wemoiso 7153 wemoiso2 7154 oprabexd 7155 omeu 7665 qliftfund 7833 eroveu 7842 fpwwe2lem11 9462 addsrmo 9894 mulsrmo 9895 seqf1o 12842 fi1uzind 13279 brfi1indALT 13282 fi1uzindOLD 13285 brfi1indALTOLD 13288 summo 14448 prodmo 14666 pceu 15551 invfun 16424 initoeu2lem2 16665 psss 17214 psgneu 17926 gsumval3eu 18305 hausflimi 21784 vitalilem3 23379 plyexmo 24068 tglineintmo 25537 frgr3vlem1 27137 3vfriswmgrlem 27141 frgr2wwlk1 27193 pjhthmo 28161 chscl 28500 bnj1379 30901 bnj580 30983 bnj1321 31095 cvmlift2lem12 31296 mclsssvlem 31459 mclsax 31466 mclsind 31467 noprefixmo 31848 nosupno 31849 lineintmo 32264 trer 32310 mbfresfi 33456 unirep 33507 iss2 34112 prter1 34164 islpoldN 36773 ismrcd2 37262 ismrc 37264 truniALT 38751 gen12 38843 sspwtrALT 39049 sspwtrALT2 39058 suctrALT 39061 suctrALT2 39072 trintALT 39117 suctrALTcf 39158 suctrALT3 39160 rlimdmafv 41257 opabresex0d 41304 spr0nelg 41726 sprsymrelfvlem 41740 |
Copyright terms: Public domain | W3C validator |