![]() |
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 3053 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜑 |
3 | mprg.1 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 ∀wral 3051 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 |
This theorem depends on definitions: df-bi 206 df-ral 3052 |
This theorem is referenced by: reximiaOLD 3078 rmoimia 3734 reuxfrd 3741 2reurmo 3752 rabxm 4387 ralf0 4514 iuneq2i 5017 iineq2i 5018 dfiun2 5036 dfiin2 5037 eusv4 5405 dfiun3 5968 dfiin3 5969 relmptopab 7669 fsplitfpar 8121 ixpint 8942 noinfep 9683 tctr 9763 r1elssi 9828 ackbij2 10266 hsmexlem5 10453 axcc2lem 10459 inar1 10798 ccatalpha 14575 sumeq2i 15677 sum2id 15686 prodeq2i 15895 prod2id 15904 prdsbasex 17431 fnmrc 17586 sscpwex 17797 gsumwspan 18802 0frgp 19738 subdrgint 20695 frgpcyg 21511 psrbaglefi 21869 psrbaglefiOLD 21870 mvrf1 21935 mplmonmul 21981 elpt 23506 ptbasin2 23512 ptbasfi 23515 ptcld 23547 ptrescn 23573 xkoinjcn 23621 ptuncnv 23741 ptunhmeo 23742 itgfsum 25786 rolle 25952 dvlip 25956 dvivthlem1 25971 dvivth 25973 pserdv 26396 logtayl 26624 goeqi 32139 reuxfrdf 32346 sxbrsigalem0 33961 bnj852 34622 bnj1145 34694 cvmsss2 34954 cvmliftphtlem 34997 dfon2lem1 35449 dfon2lem3 35451 dfon2lem7 35455 ptrest 37162 mblfinlem2 37201 voliunnfl 37207 sdclem2 37285 dmmzp 42218 arearect 42708 areaquad 42709 trclrelexplem 43206 corcltrcl 43234 cotrclrcl 43237 clsk3nimkb 43535 lhe4.4ex1a 43831 dvcosax 45377 fourierdlem57 45614 fourierdlem58 45615 fourierdlem62 45619 nnsgrpnmnd 47352 elbigofrcl 47735 iunordi 48220 |
Copyright terms: Public domain | W3C validator |