![]() |
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 1762 | . 2 ⊢ ∀𝑥𝜑 |
3 | mpg.1 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1521 |
This theorem was proved from axioms: ax-mp 5 ax-gen 1762 |
This theorem is referenced by: nfth 1767 nfnth 1768 alimi 1779 al2imi 1783 albii 1787 eximi 1802 exbii 1814 nfbii 1818 exanOLD 1829 spfwOLD 2008 nf5i 2064 hbn 2184 chvar 2298 chvarv 2299 equsb1 2396 equsb2 2397 nfsb4 2418 sbt 2447 sbtr 2449 moimi 2549 2eumo 2574 vtoclf 3289 vtocl 3290 vtocl2 3292 vtocl3 3293 spcimgf 3317 spcgf 3319 euxfr2 3424 axsep 4813 axnulALT 4820 csbex 4826 eusv2nf 4894 dtrucor 4930 ssopab2i 5032 iotabii 5911 opabiotafun 6298 eufnfv 6531 snnex 7008 pwnex 7010 tz9.13 8692 unir1 8714 axac2 9326 axpowndlem3 9459 uzrdgfni 12797 uvtx01vtx 26346 uvtxa01vtx0OLD 26348 setinds 31807 hbng 31838 bj-axd2d 32702 bj-exalimsi 32739 bj-ssbimi 32748 bj-ssbbii 32749 bj-hbsb3 32838 bj-nfs1 32841 bj-chvarv 32850 bj-chvarvv 32851 bj-equsb1v 32887 bj-sbtv 32891 bj-axsep 32918 bj-dtrucor 32925 bj-vexw 32980 bj-vexwv 32982 bj-issetw 32985 bj-abf 33028 bj-vtoclf 33033 bj-snsetex 33076 ax4fromc4 34498 ax10fromc7 34499 ax6fromc10 34500 equid1 34503 setindtrs 37909 frege97 38571 frege109 38583 pm11.11 38890 sbeqal1i 38916 axc5c4c711toc7 38922 axc5c4c711to11 38923 iotaequ 38947 setrec2lem2 42766 vsetrec 42774 |
Copyright terms: Public domain | W3C validator |