![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > mpg | Unicode 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 1562 | . 2 |
3 | mpg.1 | . 2 | |
4 | 2, 3 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: -> wi 4 A. wal 1556 |
This theorem is referenced by: alimi 1575 albii 1582 eximi 1594 exbii 1601 spfw 1710 spwOLD 1712 19.9hOLD 1794 hbn 1800 chvar 1967 chvarvOLD 1969 cbv3hOLD 1976 cbv3OLD 1977 sbt 2093 equsb1 2103 equsb2 2104 nfsb4 2131 ax4 2248 ax10 2249 ax6fromc10 2250 equid1 2260 moimi 2365 2eumo 2398 vtoclf 3055 vtocl2 3057 vtocl3 3058 spcimgf 3079 spcgf 3081 euxfr2 3170 axsep 4422 axnulALT 4429 csbex 4435 csbexOLD 4437 eusv2nf 4497 dtrucor 4532 ssopab2i 4621 iotabii 5402 opabiotafun 5745 eufnfv 5929 tz9.13 7829 unir1 7851 axac2 8460 axpowndlem3 8588 uzrdgfni 11573 setinds 26235 hbng 26266 setindtrs 28025 pm11.11 28475 sbeqal1i 28501 axc5c4c711toc7 28507 axc5c4c711to11 28508 iotaequ 28532 bj-snsetex 30670 cbv3wAUX11 30792 equsb1NEW11 30813 equsb2NEW11 30814 nfsb4wAUX11 30852 chvarNEW11 30894 chvarvNEW11 30900 cbv3OLD11 30997 cbv3hOLD11 30998 nfsb4OLD11 31021 |
This theorem was proved from axioms: ax-mp 5 ax-gen 1562 |
Copyright terms: Public domain | W3C validator |