![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE 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 1335 |
. 2
![]() ![]() ![]() ![]() |
3 | mpg.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | ax-mp 7 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 7 ax-gen 1335 |
This theorem is referenced by: alimi 1341 albii 1356 a5i 1432 eximi 1488 exbii 1493 19.9h 1531 hbn 1541 chvar 1637 equsb1 1665 equsb2 1666 chvarv 1809 moimi 1962 2eumo 1985 vtoclf 2601 vtocl2 2603 vtocl3 2604 spcimgf 2627 spcimegf 2628 spcgf 2629 spcegf 2630 mosub 2713 csbexa 3877 nalset 3878 ssopab2i 4005 eusv2nf 4154 iotabii 4832 fvmptss2 5190 eufnfv 5332 riotaexg 5415 xpcomco 6236 bj-ex 9237 ch2var 9242 bj-vtoclgf 9250 elabgf1 9253 bj-rspg 9261 bdsepnf 9343 bj-nalset 9350 setindf 9426 strcollnf 9445 |
Copyright terms: Public domain | W3C validator |