![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mprgbir | Structured version Visualization version GIF version |
Description: Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.) |
Ref | Expression |
---|---|
mprgbir.1 | ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) |
mprgbir.2 | ⊢ (𝑥 ∈ 𝐴 → 𝜓) |
Ref | Expression |
---|---|
mprgbir | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mprgbir.2 | . . 3 ⊢ (𝑥 ∈ 𝐴 → 𝜓) | |
2 | 1 | rgen 3063 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓 |
3 | mprgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbir 230 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2107 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 |
This theorem depends on definitions: df-bi 206 df-ral 3062 |
This theorem is referenced by: ss2rabi 4035 rabxm 4347 ssintub 4928 djussxp 5802 dmiin 5909 dfco2 6198 coiun 6209 tron 6341 onxpdisj 6444 epweon 7710 frrlem6 8223 frrlem7 8224 wfrrelOLD 8261 wfrdmssOLD 8262 tfrlem6 8329 oawordeulem 8502 sbthlem1 9030 marypha2lem1 9376 ttrclselem1 9666 rankval4 9808 tcwf 9824 inlresf 9855 inrresf 9857 fin23lem16 10276 fin23lem29 10282 fin23lem30 10283 itunitc 10362 acncc 10381 wfgru 10757 renfdisj 11220 ioomax 13345 iccmax 13346 hashgval2 14284 fsumcom2 15664 fprodcom2 15872 dfphi2 16651 oppccatf 17615 dmcoass 17957 letsr 18487 smndex2dnrinv 18730 efgsf 19516 lssuni 20415 lpival 20731 cnsubdrglem 20864 retos 21038 psr1baslem 21572 istopon 22277 neips 22480 filssufilg 23278 xrhmeo 24325 iscmet3i 24692 ehlbase 24795 ovolge0 24861 unidmvol 24921 resinf1o 25908 divlogrlim 26006 dvloglem 26019 logf1o2 26021 atansssdm 26299 ppiub 26568 bday1s 27192 lrrecse 27276 clwwlkn0 29014 sspval 29707 shintcli 30313 lnopco0i 30988 imaelshi 31042 nmopadjlem 31073 nmoptrii 31078 nmopcoi 31079 nmopcoadji 31085 idleop 31115 hmopidmchi 31135 hmopidmpji 31136 djussxp2 31610 xrsclat 31920 rearchi 32185 dmvlsiga 32785 sxbrsigalem0 32928 dya2iocucvr 32941 eulerpartlemgh 33035 bnj110 33527 subfacp1lem1 33830 erdszelem2 33843 dfon2lem3 34416 filnetlem2 34897 taupi 35840 cnviun 42010 coiun1 42012 comptiunov2i 42066 cotrcltrcl 42085 cotrclrcl 42102 ssrab2f 43415 iooinlbub 43825 stirlinglem14 44414 sssalgen 44662 fvmptrabdm 45611 unilbss 46988 |
Copyright terms: Public domain | W3C validator |