Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mprg | Structured version Visualization version GIF 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 3145 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜑 |
3 | mprg.1 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 |
This theorem depends on definitions: df-bi 208 df-ral 3140 |
This theorem is referenced by: reximia 3239 rmoimia 3729 reuxfrd 3736 2reurmo 3748 iuneq2i 4931 iineq2i 4932 dfiun2 4949 dfiin2 4950 eusv4 5297 dfiun3 5830 dfiin3 5831 relmptopab 7384 fsplitfpar 7803 ixpint 8477 noinfep 9111 tctr 9170 r1elssi 9222 ackbij2 9653 hsmexlem5 9840 axcc2lem 9846 inar1 10185 ccatalpha 13935 sumeq2i 15044 sum2id 15053 prodeq2i 15261 prod2id 15270 prdsbasex 16712 fnmrc 16866 sscpwex 17073 gsumwspan 17999 0frgp 18834 subdrgint 19511 psrbaglefi 20080 mvrf1 20133 mplmonmul 20173 frgpcyg 20648 elpt 22108 ptbasin2 22114 ptbasfi 22117 ptcld 22149 ptrescn 22175 xkoinjcn 22223 ptuncnv 22343 ptunhmeo 22344 itgfsum 24354 rolle 24514 dvlip 24517 dvivthlem1 24532 dvivth 24534 pserdv 24944 logtayl 25170 goeqi 29977 reuxfrdf 30182 sxbrsigalem0 31428 bnj852 32092 bnj1145 32162 cvmsss2 32418 cvmliftphtlem 32461 dfon2lem1 32925 dfon2lem3 32927 dfon2lem7 32931 ptrest 34772 mblfinlem2 34811 voliunnfl 34817 sdclem2 34898 dmmzp 39208 arearect 39700 areaquad 39701 trclrelexplem 39934 corcltrcl 39962 cotrclrcl 39965 clsk3nimkb 40268 lhe4.4ex1a 40538 dvcosax 42087 fourierdlem57 42325 fourierdlem58 42326 fourierdlem62 42330 nnsgrpnmnd 43962 elbigofrcl 44538 iunordi 44708 |
Copyright terms: Public domain | W3C validator |