![]() |
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 1798 | . 2 ⊢ ∀𝑥𝜑 |
3 | mpg.1 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-gen 1798 |
This theorem is referenced by: nfth 1804 nfnth 1805 alimi 1814 al2imi 1818 albii 1822 eximi 1838 exbii 1851 nfbii 1855 chvarvv 2003 sbtALT 2073 sbn1 2106 nf5i 2143 chvarfv 2234 hbn 2292 chvar 2395 equsb1 2491 equsb2 2492 nfsb4 2500 sbtr 2516 2eumo 2639 abbii 2803 vtoclfOLD 3549 spcimgf 3580 spcgf 3582 euxfr2w 3716 euxfr2 3718 noel 4330 axsepgfromrep 5297 axnulALT 5304 csbex 5311 dtrucor 5369 eusv2nf 5393 axprlem3 5423 ssopab2i 5550 iotabii 6526 opabiotafun 6970 eufnfv 7228 snnex 7742 pwnex 7743 tz9.13 9783 unir1 9805 axac2 10458 axpowndlem3 10591 uzrdgfni 13920 uvtx01vtx 28644 setinds 34739 hbng 34769 bj-axd2d 35460 bj-exalimsi 35501 bj-hbsb3 35656 bj-nfs1 35659 sbn1ALT 35726 bj-issetw 35744 bj-abf 35778 bj-vtoclf 35784 bj-snsetex 35833 ax4fromc4 37753 ax10fromc7 37754 ax6fromc10 37755 equid1 37758 sn-axprlem3 41031 setindtrs 41750 frege97 42697 frege109 42709 pm11.11 43119 sbeqal1i 43144 axc5c4c711toc7 43149 axc5c4c711to11 43150 iotaequ 43174 mof0 47458 setrec2lem2 47693 vsetrec 47702 |
Copyright terms: Public domain | W3C validator |