![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpg | Structured version Visualization version GIF version |
Description: Modus ponens combined with generalization. (Contributed by NM, 24-May-1994.) |
Ref | Expression |
---|---|
mpg.1 | ⊢ (∀𝑥𝜑 → 𝜓) |
mpg.2 | ⊢ 𝜑 |
Ref | Expression |
---|---|
mpg | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpg.2 | . . 3 ⊢ 𝜑 | |
2 | 1 | ax-gen 1863 | . 2 ⊢ ∀𝑥𝜑 |
3 | mpg.1 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1622 |
This theorem was proved from axioms: ax-mp 5 ax-gen 1863 |
This theorem is referenced by: nfth 1868 nfnth 1869 alimi 1880 al2imi 1884 albii 1888 eximi 1903 exbii 1915 nfbii 1919 exanOLD 1930 spfwOLD 2109 nf5i 2165 hbn 2285 chvar 2399 chvarv 2400 equsb1 2497 equsb2 2498 nfsb4 2519 sbt 2548 sbtr 2550 moimi 2650 2eumo 2675 vtoclf 3390 vtocl 3391 vtocl2 3393 vtocl3 3394 spcimgf 3418 spcgf 3420 euxfr2 3524 axsep 4924 axnulALT 4931 csbex 4937 eusv2nf 5005 dtrucor 5041 ssopab2i 5145 iotabii 6026 opabiotafun 6413 eufnfv 6646 snnex 7123 pwnex 7125 tz9.13 8819 unir1 8841 axac2 9472 axpowndlem3 9605 uzrdgfni 12943 uvtx01vtx 26492 uvtxa01vtx0OLD 26494 setinds 31980 hbng 32011 bj-axd2d 32875 bj-exalimsi 32912 bj-ssbimi 32921 bj-ssbbii 32922 bj-hbsb3 33011 bj-nfs1 33014 bj-chvarv 33023 bj-chvarvv 33024 bj-equsb1v 33060 bj-sbtv 33064 bj-axsep 33091 bj-dtrucor 33098 bj-vexw 33153 bj-vexwv 33155 bj-issetw 33158 bj-abf 33201 bj-vtoclf 33206 bj-snsetex 33249 ax4fromc4 34675 ax10fromc7 34676 ax6fromc10 34677 equid1 34680 setindtrs 38086 frege97 38748 frege109 38760 pm11.11 39067 sbeqal1i 39093 axc5c4c711toc7 39099 axc5c4c711to11 39100 iotaequ 39124 setrec2lem2 42943 vsetrec 42951 |
Copyright terms: Public domain | W3C validator |