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 1803 | . 2 ⊢ ∀𝑥𝜑 |
3 | mpg.1 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1541 |
This theorem was proved from axioms: ax-mp 5 ax-gen 1803 |
This theorem is referenced by: nfth 1809 nfnth 1810 alimi 1819 al2imi 1823 albii 1827 eximi 1842 exbii 1855 nfbii 1859 chvarvv 2007 sbtALT 2075 sbn1 2109 nf5i 2146 chvarfv 2238 hbn 2296 chvar 2394 equsb1 2494 equsb2 2495 nfsb4 2503 sbtr 2519 2eumo 2643 abbii 2808 vtoclf 3478 spcimgf 3509 spcgf 3511 euxfr2w 3638 euxfr2 3640 noel 4250 axsepgfromrep 5195 axnulALT 5202 csbex 5209 dtrucor 5269 eusv2nf 5293 axprlem3 5323 ssopab2i 5436 iotabii 6370 opabiotafun 6797 eufnfv 7050 snnex 7548 pwnex 7549 tz9.13 9412 unir1 9434 axac2 10085 axpowndlem3 10218 uzrdgfni 13536 uvtx01vtx 27490 setinds 33478 hbng 33508 bj-axd2d 34517 bj-exalimsi 34558 bj-hbsb3 34713 bj-nfs1 34716 sbn1ALT 34784 bj-issetw 34802 bj-abf 34836 bj-vtoclf 34842 bj-snsetex 34895 ax4fromc4 36650 ax10fromc7 36651 ax6fromc10 36652 equid1 36655 sn-axprlem3 39916 setindtrs 40558 frege97 41253 frege109 41265 pm11.11 41673 sbeqal1i 41698 axc5c4c711toc7 41703 axc5c4c711to11 41704 iotaequ 41728 mof0 45846 setrec2lem2 46079 vsetrec 46087 |
Copyright terms: Public domain | W3C validator |