| 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 3063 | . 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 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 |
| This theorem depends on definitions: df-bi 207 df-ral 3062 |
| This theorem is referenced by: reximiaOLD 3088 rmoimia 3747 reuxfrd 3754 2reurmo 3765 rabxm 4390 ralf0 4514 iuneq2i 5013 iineq2i 5014 dfiun2 5033 dfiin2 5034 eusv4 5406 dfiun3 5980 dfiin3 5981 relmptopab 7683 fsplitfpar 8143 ixpint 8965 noinfep 9700 tctr 9780 r1elssi 9845 ackbij2 10282 hsmexlem5 10470 axcc2lem 10476 inar1 10815 ccatalpha 14631 sumeq2i 15734 sum2id 15744 prodeq2i 15954 prod2id 15964 prdsbasex 17495 fnmrc 17650 sscpwex 17859 gsumwspan 18859 0frgp 19797 subdrgint 20804 frgpcyg 21592 psrbaglefi 21946 mvrf1 22006 mplmonmul 22054 elpt 23580 ptbasin2 23586 ptbasfi 23589 ptcld 23621 ptrescn 23647 xkoinjcn 23695 ptuncnv 23815 ptunhmeo 23816 itgfsum 25862 rolle 26028 dvlip 26032 dvivthlem1 26047 dvivth 26049 pserdv 26473 logtayl 26702 goeqi 32292 reuxfrdf 32510 sxbrsigalem0 34273 bnj852 34935 bnj1145 35007 cvmsss2 35279 cvmliftphtlem 35322 dfon2lem1 35784 dfon2lem3 35786 dfon2lem7 35790 disjeq12i 36194 ptrest 37626 mblfinlem2 37665 voliunnfl 37671 sdclem2 37749 dmmzp 42744 arearect 43227 areaquad 43228 trclrelexplem 43724 corcltrcl 43752 cotrclrcl 43755 clsk3nimkb 44053 lhe4.4ex1a 44348 wfaxsep 45012 wfaxpow 45014 wfaxun 45016 dvcosax 45941 fourierdlem57 46178 fourierdlem58 46179 fourierdlem62 46183 nnsgrpnmnd 48094 elbigofrcl 48471 iunordi 49196 |
| Copyright terms: Public domain | W3C validator |