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 2062 and 19.21v 1855. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimivv | ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | alrimiv 1842 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1842 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem is referenced by: 2ax5 1853 2mo 2539 euind 3360 sbnfc2 3959 uniintsn 4449 eusvnf 4787 ssopab2dv 4929 ssrel 5130 ssrelOLD 5131 relssdv 5135 eqrelrdv 5139 eqbrrdv 5140 eqrelrdv2 5142 ssrelrel 5143 iss 5367 ordelord 5662 suctr 5725 suctrOLD 5726 funssres 5844 funun 5846 fununi 5878 fsn 6308 ovg 6697 wemoiso 7044 wemoiso2 7045 oprabexd 7046 omeu 7552 qliftfund 7720 eroveu 7729 fpwwe2lem11 9341 addsrmo 9773 mulsrmo 9774 seqf1o 12704 fi1uzind 13134 brfi1indALT 13137 fi1uzindOLD 13140 brfi1indALTOLD 13143 summo 14295 prodmo 14505 pceu 15389 invfun 16247 initoeu2lem2 16488 psss 17037 psgneu 17749 gsumval3eu 18128 hausflimi 21594 vitalilem3 23185 plyexmo 23872 tglineintmo 25337 frgra3vlem1 26527 3vfriswmgralem 26531 frg2wot1 26584 2spotdisj 26588 pjhthmo 27545 chscl 27884 bnj1379 30155 bnj580 30237 bnj1321 30349 cvmlift2lem12 30550 mclsssvlem 30713 mclsax 30720 mclsind 30721 lineintmo 31434 trer 31480 mbfresfi 32626 unirep 32677 prter1 33182 islpoldN 35791 ismrcd2 36280 ismrc 36282 truniALT 37772 gen12 37864 sspwtrALT 38071 sspwtrALT2 38080 suctrALT 38083 suctrALT2 38094 trintALT 38139 suctrALTcf 38180 suctrALT3 38182 rlimdmafv 39906 opabresex0d 40330 opabresex2d 40334 frgr3vlem1 41443 3vfriswmgrlem 41447 frgr2wwlk1 41494 |
Copyright terms: Public domain | W3C validator |