![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mprg | Structured version Visualization version 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 2747 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | mprg.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | ax-mp 5 |
1
![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 |
This theorem depends on definitions: df-bi 189 df-ral 2742 |
This theorem is referenced by: reximia 2853 rmoimia 3240 iuneq2i 4297 iineq2i 4298 dfiun2 4312 dfiin2 4313 eusv4 4612 reuxfr2d 4623 dfiun3 5089 dfiin3 5090 cnviin 5373 relmptopab 6517 ixpint 7549 noinfep 8165 tctr 8224 r1elssi 8276 ackbij2 8673 hsmexlem5 8860 axcc2lem 8866 inar1 9200 sumeq2i 13765 sum2id 13774 prodeq2i 13973 prod2id 13982 prdsbasex 15349 fnmrc 15513 sscpwex 15720 gsumwspan 16630 0frgp 17429 psrbaglefi 18596 mvrf1 18649 mplmonmul 18688 frgpcyg 19144 elpt 20587 ptbasin2 20593 ptbasfi 20596 ptcld 20628 ptrescn 20654 xkoinjcn 20702 ptuncnv 20822 ptunhmeo 20823 itgfsum 22784 rolle 22942 dvlip 22945 dvivthlem1 22960 dvivth 22962 pserdv 23384 logtayl 23605 goeqi 27926 reuxfr3d 28125 sxbrsigalem0 29093 bnj852 29732 bnj1145 29802 cvmsss2 29997 cvmliftphtlem 30040 dfon2lem1 30429 dfon2lem3 30431 dfon2lem7 30435 ptrest 31939 mblfinlem2 31978 voliunnfl 31984 sdclem2 32071 dmmzp 35575 arearect 36100 areaquad 36101 trclrelexplem 36303 corcltrcl 36331 cotrclrcl 36334 lhe4.4ex1a 36678 dvcosax 37798 fourierdlem57 38027 fourierdlem58 38028 fourierdlem62 38032 2reurmo 38603 nnsgrpnmnd 39871 elbigofrcl 40414 |
Copyright terms: Public domain | W3C validator |