![]() |
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 1942. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimivv | ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | alrimiv 1930 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1930 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1797 ax-4 1811 ax-5 1913 |
This theorem is referenced by: 2ax5 1940 2mo 2648 euind 3680 sbnfc2 4394 uniintsn 4946 eusvnf 5345 ssopab2dv 5506 ssrel 5736 ssrelOLD 5737 relssdv 5742 eqrelrdv 5746 eqbrrdv 5747 eqrelrdv2 5749 ssrelrel 5750 iss 5987 iresn0n0 6005 ordelord 6337 suctr 6401 funssres 6542 funun 6544 fununi 6573 fsn 7077 opabresex2d 7406 fvmptopabOLD 7408 ovg 7515 wemoiso 7902 wemoiso2 7903 oprabexd 7904 frrlem9 8221 omeu 8528 qliftfund 8738 eroveu 8747 fpwwe2lem10 10572 addsrmo 11005 mulsrmo 11006 seqf1o 13941 fi1uzind 14388 brfi1indALT 14391 summo 15594 prodmo 15811 pceu 16710 invfun 17639 initoeu2lem2 17893 psss 18461 psgneu 19279 gsumval3eu 19672 hausflimi 23315 vitalilem3 24958 plyexmo 25657 nosupprefixmo 27032 noinfprefixmo 27033 nosupno 27035 noinfno 27050 tglineintmo 27470 frgr3vlem1 29103 3vfriswmgrlem 29107 frgr2wwlk1 29159 pjhthmo 30130 chscl 30469 bnj1379 33311 bnj580 33394 bnj1321 33508 acycgr1v 33612 cvmlift2lem12 33777 satffunlem1lem1 33865 satffunlem2lem1 33867 mclsssvlem 34025 mclsax 34032 mclsind 34033 lineintmo 34709 trer 34755 mbfresfi 36091 unirep 36139 iss2 36772 prter1 37308 islpoldN 39914 ismrcd2 40960 ismrc 40962 mnutrd 42502 truniALT 42765 gen12 42842 sspwtrALT 43046 sspwtrALT2 43047 suctrALT 43050 suctrALT2 43061 trintALT 43105 suctrALTcf 43146 suctrALT3 43148 rlimdmafv 45341 rlimdmafv2 45422 opabresex0d 45449 spr0nelg 45600 sprsymrelfvlem 45614 mofsn 46842 thincmo 46981 |
Copyright terms: Public domain | W3C validator |