![]() |
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 2205 and 19.21v 1937. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimivv | ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | alrimiv 1925 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1925 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1792 ax-4 1806 ax-5 1908 |
This theorem is referenced by: 2ax5 1935 2mo 2646 euind 3733 sbnfc2 4445 uniintsn 4990 eusvnf 5398 ssopab2dv 5561 ssrel 5795 ssrelOLD 5796 relssdv 5801 eqrelrdv 5805 eqbrrdv 5806 eqrelrdv2 5808 ssrelrel 5809 iss 6055 iresn0n0 6074 ordelord 6408 suctr 6472 funssres 6612 funun 6614 fununi 6643 fsn 7155 opabresex2d 7486 fvmptopabOLD 7488 ovg 7598 wemoiso 7997 wemoiso2 7998 oprabexd 7999 frrlem9 8318 omeu 8622 qliftfund 8842 eroveu 8851 fpwwe2lem10 10678 addsrmo 11111 mulsrmo 11112 seqf1o 14081 fi1uzind 14543 brfi1indALT 14546 summo 15750 prodmo 15969 pceu 16880 invfun 17812 initoeu2lem2 18069 psss 18638 psgneu 19539 gsumval3eu 19937 hausflimi 24004 vitalilem3 25659 plyexmo 26370 nosupprefixmo 27760 noinfprefixmo 27761 nosupno 27763 noinfno 27778 tglineintmo 28665 frgr3vlem1 30302 3vfriswmgrlem 30306 frgr2wwlk1 30358 pjhthmo 31331 chscl 31670 copsex2dv 32626 bnj1379 34823 bnj580 34906 bnj1321 35020 acycgr1v 35134 cvmlift2lem12 35299 satffunlem1lem1 35387 satffunlem2lem1 35389 mclsssvlem 35547 mclsax 35554 mclsind 35555 lineintmo 36139 trer 36299 mbfresfi 37653 unirep 37701 iss2 38326 prter1 38861 islpoldN 41467 ismrcd2 42687 ismrc 42689 tfsconcatb0 43334 mnutrd 44276 truniALT 44539 gen12 44616 sspwtrALT 44820 sspwtrALT2 44821 suctrALT 44824 suctrALT2 44835 trintALT 44879 suctrALTcf 44920 suctrALT3 44922 rlimdmafv 47127 rlimdmafv2 47208 opabresex0d 47235 spr0nelg 47401 sprsymrelfvlem 47415 mofsn 48674 thincmo 48829 |
Copyright terms: Public domain | W3C validator |