New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 1546 | . 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 1546 |
This theorem is referenced by: alimi 1559 albii 1566 eximi 1576 exbii 1582 spfw 1691 spw 1694 hbn 1776 19.9hOLD 1781 cbv3 1982 cbv3h 1983 chvar 1986 chvarv 2013 equsb1 2034 equsb2 2035 nfsb4 2081 ax5 2146 ax6 2147 ax9from9o 2148 equid1 2158 moimi 2251 2eumo 2277 vtoclf 2908 vtocl2 2910 vtocl3 2911 spcimgf 2932 spcgf 2934 euxfr2 3021 csbex 3147 iotabii 4361 ssopab2i 4714 |
Copyright terms: Public domain | W3C validator |