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 3146 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜑 |
3 | mprg.1 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2108 ∀wral 3136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 |
This theorem depends on definitions: df-bi 209 df-ral 3141 |
This theorem is referenced by: reximia 3240 rmoimia 3730 reuxfrd 3737 2reurmo 3749 iuneq2i 4931 iineq2i 4932 dfiun2 4949 dfiin2 4950 eusv4 5297 dfiun3 5830 dfiin3 5831 relmptopab 7387 fsplitfpar 7806 ixpint 8481 noinfep 9115 tctr 9174 r1elssi 9226 ackbij2 9657 hsmexlem5 9844 axcc2lem 9850 inar1 10189 ccatalpha 13939 sumeq2i 15048 sum2id 15057 prodeq2i 15265 prod2id 15274 prdsbasex 16716 fnmrc 16870 sscpwex 17077 gsumwspan 18003 0frgp 18897 subdrgint 19574 psrbaglefi 20144 mvrf1 20197 mplmonmul 20237 frgpcyg 20712 elpt 22172 ptbasin2 22178 ptbasfi 22181 ptcld 22213 ptrescn 22239 xkoinjcn 22287 ptuncnv 22407 ptunhmeo 22408 itgfsum 24419 rolle 24579 dvlip 24582 dvivthlem1 24597 dvivth 24599 pserdv 25009 logtayl 25235 goeqi 30042 reuxfrdf 30247 sxbrsigalem0 31522 bnj852 32186 bnj1145 32258 cvmsss2 32514 cvmliftphtlem 32557 dfon2lem1 33021 dfon2lem3 33023 dfon2lem7 33027 ptrest 34883 mblfinlem2 34922 voliunnfl 34928 sdclem2 35009 dmmzp 39321 arearect 39813 areaquad 39814 trclrelexplem 40047 corcltrcl 40075 cotrclrcl 40078 clsk3nimkb 40381 lhe4.4ex1a 40652 dvcosax 42201 fourierdlem57 42439 fourierdlem58 42440 fourierdlem62 42444 nnsgrpnmnd 44076 elbigofrcl 44601 iunordi 44771 |
Copyright terms: Public domain | W3C validator |