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 2906 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓 |
3 | mprgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbir 220 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 |
This theorem depends on definitions: df-bi 196 df-ral 2901 |
This theorem is referenced by: ss2rabi 3647 rabxm 3915 ssintub 4430 djussxp 5189 dmiin 5290 dfco2 5551 coiun 5562 tron 5663 onxpdisj 5764 wfrrel 7307 wfrdmss 7308 tfrlem6 7365 oawordeulem 7521 sbthlem1 7955 marypha2lem1 8224 rankval4 8613 tcwf 8629 fin23lem16 9040 fin23lem29 9046 fin23lem30 9047 itunitc 9126 acncc 9145 wfgru 9517 renfdisj 9977 ioomax 12119 iccmax 12120 hashgval2 13028 fsumcom2 14347 fsumcom2OLD 14348 fprodcom2 14553 fprodcom2OLD 14554 dfphi2 15317 dmcoass 16539 letsr 17050 efgsf 17965 lssuni 18761 lpival 19066 psr1baslem 19376 cnsubdrglem 19616 retos 19783 istopon 20540 neips 20727 filssufilg 21525 xrhmeo 22553 iscmet3i 22918 ehlbase 23002 ovolge0 23056 unidmvol 23116 resinf1o 24086 divlogrlim 24181 dvloglem 24194 logf1o2 24196 atansssdm 24460 ppiub 24729 sspval 26962 shintcli 27572 lnopco0i 28247 imaelshi 28301 nmopadjlem 28332 nmoptrii 28337 nmopcoi 28338 nmopcoadji 28344 idleop 28374 hmopidmchi 28394 hmopidmpji 28395 xrsclat 29011 rearchi 29173 dmvlsiga 29519 sxbrsigalem0 29660 dya2iocucvr 29673 eulerpartlemgh 29767 bnj110 30182 subfacp1lem1 30415 erdszelem2 30428 dfon2lem3 30934 trpredlem1 30971 frrlem6 31033 frrlem7 31034 nofulllem5 31105 filnetlem2 31544 taupi 32346 cnviun 36961 coiun1 36963 comptiunov2i 37017 cotrcltrcl 37036 cotrclrcl 37053 iooinlbub 38570 stirlinglem14 38980 sssalgen 39229 |
Copyright terms: Public domain | W3C validator |