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 1713 | . 2 ⊢ ∀𝑥𝜑 |
3 | mpg.1 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-gen 1713 |
This theorem is referenced by: nfth 1718 nfnth 1719 alimi 1730 al2imi 1733 albii 1737 eximi 1752 exbii 1764 exanOLD 1776 spfwOLD 1953 nf5i 2011 hbn 2131 chvar 2250 chvarv 2251 equsb1 2356 equsb2 2357 nfsb4 2378 sbt 2407 sbtr 2409 moimi 2508 2eumo 2533 vtoclf 3231 vtocl 3232 vtocl2 3234 vtocl3 3235 spcimgf 3259 spcgf 3261 euxfr2 3358 axsep 4708 axnulALT 4715 csbex 4721 eusv2nf 4790 dtrucor 4827 ssopab2i 4928 iotabii 5790 opabiotafun 6169 eufnfv 6395 tz9.13 8537 unir1 8559 axac2 9171 axpowndlem3 9300 uzrdgfni 12619 setinds 30927 hbng 30958 bj-axd2d 31750 bj-nfth 31772 bj-nfnth 31774 bj-nfxfr 31794 bj-ssbimi 31812 bj-ssbbii 31813 bj-hbsb3 31900 bj-nfs1 31903 bj-chvarv 31912 bj-chvarvv 31913 bj-equsb1v 31950 bj-sbtv 31954 bj-axsep 31981 bj-dtrucor 31988 bj-vexw 32049 bj-vexwv 32051 bj-issetw 32054 bj-abf 32095 bj-vtoclf 32100 bj-snsetex 32144 bj-pwnex 32246 ax4fromc4 33197 ax10fromc7 33198 ax6fromc10 33199 equid1 33202 setindtrs 36610 frege97 37274 frege109 37286 pm11.11 37595 sbeqal1i 37621 axc5c4c711toc7 37627 axc5c4c711to11 37628 iotaequ 37652 uvtxa01vtx0 40623 setrec2lem2 42240 vsetrec 42245 |
Copyright terms: Public domain | W3C validator |