![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpg | Structured version Visualization version Unicode 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 1679 |
. 2
![]() ![]() ![]() ![]() |
3 | mpg.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | ax-mp 5 |
1
![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-gen 1679 |
This theorem is referenced by: alimi 1694 al2imi 1697 albii 1701 eximi 1717 exbii 1728 spfw 1885 hbn 1987 chvar 2116 equsb1 2207 equsb2 2208 nfsb4 2229 sbt 2258 sbtr 2260 moimi 2359 2eumo 2384 vtoclf 3110 vtocl 3111 vtocl2 3113 vtocl3 3114 spcimgf 3138 spcgf 3140 euxfr2 3234 axsep 4537 axnulALT 4544 csbex 4551 eusv2nf 4614 dtrucor 4646 ssopab2i 4742 iotabii 5586 opabiotafun 5948 eufnfv 6163 tz9.13 8287 unir1 8309 axac2 8921 axpowndlem3 9049 uzrdgfni 12203 setinds 30472 hbng 30503 bj-axd2d 31220 bj-nfth 31242 bj-nfnth 31244 bj-nfxfr 31262 bj-ssbimi 31280 bj-ssbbii 31281 bj-hbsb3 31358 bj-nfs1 31361 bj-chvarv 31370 bj-chvarvv 31371 bj-equsb1v 31419 bj-sbtv 31422 bj-axsep 31452 bj-dtrucor 31459 bj-vexw 31508 bj-vexwv 31510 bj-issetw 31513 bj-abf 31554 bj-vtoclf 31559 bj-snsetex 31601 ax4 32510 ax10 32511 ax6fromc10 32512 equid1 32522 setindtrs 35924 frege97 36600 frege109 36612 pm11.11 36766 sbeqal1i 36792 axc5c4c711toc7 36798 axc5c4c711to11 36799 iotaequ 36823 uvtxa01vtx0 39518 |
Copyright terms: Public domain | W3C validator |