![]() |
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 3055 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓 |
3 | mprgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbir 230 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2098 ∀wral 3053 |
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 3054 |
This theorem is referenced by: ss2rabi 4067 rabxm 4379 ssintub 4961 djussxp 5836 dmiin 5943 dfco2 6235 coiun 6246 tron 6378 onxpdisj 6481 epweon 7756 frrlem6 8272 frrlem7 8273 wfrrelOLD 8310 wfrdmssOLD 8311 tfrlem6 8378 oawordeulem 8550 sbthlem1 9080 marypha2lem1 9427 ttrclselem1 9717 rankval4 9859 tcwf 9875 inlresf 9906 inrresf 9908 fin23lem16 10327 fin23lem29 10333 fin23lem30 10334 itunitc 10413 acncc 10432 wfgru 10808 renfdisj 11272 ioomax 13397 iccmax 13398 hashgval2 14336 fsumcom2 15718 fprodcom2 15926 dfphi2 16708 oppccatf 17675 dmcoass 18020 letsr 18550 smndex2dnrinv 18832 efgsf 19641 lssuni 20778 lpival 21169 cnsubdrglem 21282 retos 21481 psr1baslem 22029 istopon 22738 neips 22941 filssufilg 23739 xrhmeo 24795 iscmet3i 25164 ehlbase 25267 ovolge0 25334 unidmvol 25394 resinf1o 26389 divlogrlim 26488 dvloglem 26501 logf1o2 26503 atansssdm 26784 ppiub 27056 bday1s 27683 lrrecse 27778 clwwlkn0 29753 sspval 30448 shintcli 31054 lnopco0i 31729 imaelshi 31783 nmopadjlem 31814 nmoptrii 31819 nmopcoi 31820 nmopcoadji 31826 idleop 31856 hmopidmchi 31876 hmopidmpji 31877 djussxp2 32345 xrsclat 32651 rearchi 32930 dmvlsiga 33619 sxbrsigalem0 33762 dya2iocucvr 33775 eulerpartlemgh 33869 bnj110 34360 subfacp1lem1 34661 erdszelem2 34674 dfon2lem3 35253 filnetlem2 35755 taupi 36695 cnviun 42915 coiun1 42917 comptiunov2i 42971 cotrcltrcl 42990 cotrclrcl 43007 ssrab2f 44319 iooinlbub 44724 stirlinglem14 45313 sssalgen 45561 fvmptrabdm 46511 unilbss 47714 |
Copyright terms: Public domain | W3C validator |