![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > mprg | Unicode version |
Description: Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.) |
Ref | Expression |
---|---|
mprg.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mprg.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mprg |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mprg.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | rgen 2739 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | mprg.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | ax-mp 8 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem is referenced by: reximia 2779 rmoimia 3102 iuneq2i 4079 iineq2i 4080 dfiun2 4093 dfiin2 4094 eusv4 4699 reuxfr2d 4713 dfiun3 5091 dfiin3 5092 cnviin 5376 relmptopab 6259 ixpint 7056 noinfep 7578 tctr 7643 r1elssi 7695 ackbij2 8087 hsmexlem5 8274 axcc2lem 8280 inar1 8614 sumeq2i 12456 sum2id 12465 prdsbasex 13637 fnmrc 13795 sscpwex 13978 gsumwspan 14754 0frgp 15374 psrbaglefi 16400 mvrf1 16452 mplmonmul 16490 frgpcyg 16817 elpt 17565 ptbasin2 17571 ptbasfi 17574 ptcld 17606 ptrescn 17632 xkoinjcn 17680 ptuncnv 17800 ptunhmeo 17801 itgfsum 19679 rolle 19835 dvlip 19838 dvivthlem1 19853 dvivth 19855 pserdv 20306 logtayl 20512 goeqi 23737 reuxfr3d 23937 sxbrsigalem0 24582 cvmsss2 24922 cvmliftphtlem 24965 prodeq2i 25206 prod2id 25215 dfon2lem1 25361 dfon2lem3 25363 dfon2lem7 25367 mblfinlem 26151 voliunnfl 26157 sdclem2 26344 dmmzp 26688 lhe4.4ex1a 27422 2reurmo 27835 bnj852 29010 bnj1145 29080 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 |
This theorem depends on definitions: df-bi 178 df-ral 2679 |
Copyright terms: Public domain | W3C validator |