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 2198 and 19.21v 1931. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimivv | ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | alrimiv 1919 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1919 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1787 ax-4 1801 ax-5 1902 |
This theorem is referenced by: 2ax5 1929 2mo 2729 euind 3714 sbnfc2 4387 uniintsn 4906 eusvnf 5284 ssopab2dv 5430 ssrel 5651 relssdv 5655 eqrelrdv 5659 eqbrrdv 5660 eqrelrdv2 5662 ssrelrel 5663 iss 5897 iresn0n0 5917 ordelord 6207 suctr 6268 funssres 6392 funun 6394 fununi 6423 fsn 6890 opabresex2d 7197 fvmptopab 7198 ovg 7302 wemoiso 7665 wemoiso2 7666 oprabexd 7667 omeu 8201 qliftfund 8373 eroveu 8382 fpwwe2lem11 10051 addsrmo 10484 mulsrmo 10485 seqf1o 13401 fi1uzind 13845 brfi1indALT 13848 summo 15064 prodmo 15280 pceu 16173 invfun 17024 initoeu2lem2 17265 psss 17814 psgneu 18565 gsumval3eu 18955 hausflimi 22518 vitalilem3 24140 plyexmo 24831 tglineintmo 26356 frgr3vlem1 27980 3vfriswmgrlem 27984 frgr2wwlk1 28036 pjhthmo 29007 chscl 29346 bnj1379 32002 bnj580 32085 bnj1321 32197 acycgr1v 32294 cvmlift2lem12 32459 satffunlem1lem1 32547 satffunlem2lem1 32549 mclsssvlem 32707 mclsax 32714 mclsind 32715 frrlem9 33029 noprefixmo 33100 nosupno 33101 lineintmo 33516 trer 33562 mbfresfi 34820 unirep 34871 iss2 35484 prter1 35897 islpoldN 38502 ismrcd2 39176 ismrc 39178 mnutrd 40496 truniALT 40755 gen12 40832 sspwtrALT 41036 sspwtrALT2 41037 suctrALT 41040 suctrALT2 41051 trintALT 41095 suctrALTcf 41136 suctrALT3 41138 rlimdmafv 43257 rlimdmafv2 43338 opabresex0d 43365 spr0nelg 43485 sprsymrelfvlem 43499 |
Copyright terms: Public domain | W3C validator |