| 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 1795 | . 2 ⊢ ∀𝑥𝜑 |
| 3 | mpg.1 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) | |
| 4 | 2, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 |
| This theorem was proved from axioms: ax-mp 5 ax-gen 1795 |
| This theorem is referenced by: nfth 1801 nfnth 1802 alimi 1811 al2imi 1815 albii 1819 eximi 1835 exbii 1848 nfbii 1852 chvarvv 1998 sbtALT 2069 sbn1 2107 nf5i 2146 chvarfv 2240 hbn 2295 chvar 2400 equsb1 2496 equsb2 2497 nfsb4 2505 sbtr 2521 2eumo 2642 abbii 2809 spcimgf 3550 vtoclfOLD 3565 spcgf 3591 euxfr2w 3726 euxfr2 3728 noel 4338 axsepgfromrep 5294 axnulALT 5304 csbex 5311 dtrucor 5371 eusv2nf 5395 axprlem3 5425 axprlem3OLD 5428 ssopab2i 5555 iotabii 6546 opabiotafun 6989 eufnfv 7249 snnex 7778 pwnex 7779 tz9.13 9831 unir1 9853 axac2 10506 axpowndlem3 10639 uzrdgfni 13999 uvtx01vtx 29414 setinds 35779 hbng 35809 bj-axd2d 36594 bj-exalimsi 36636 bj-hbsb3 36790 bj-nfs1 36793 sbn1ALT 36859 bj-issetw 36877 bj-abf 36910 bj-vtoclf 36916 bj-snsetex 36964 ax4fromc4 38895 ax10fromc7 38896 ax6fromc10 38897 equid1 38900 sn-axprlem3 42256 setindtrs 43037 frege97 43973 frege109 43985 pm11.11 44393 sbeqal1i 44418 axc5c4c711toc7 44423 axc5c4c711to11 44424 iotaequ 44448 mof0 48747 setrec2lem2 49213 vsetrec 49222 |
| Copyright terms: Public domain | W3C validator |