![]() |
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 3114 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓 |
3 | mprgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbir 232 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∈ wcel 2080 ∀wral 3104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 |
This theorem depends on definitions: df-bi 208 df-ral 3109 |
This theorem is referenced by: ss2rabi 3976 rabxm 4262 ssintub 4802 djussxp 5605 dmiin 5710 dfco2 5976 coiun 5987 tron 6092 onxpdisj 6188 wfrrel 7815 wfrdmss 7816 tfrlem6 7873 oawordeulem 8033 sbthlem1 8477 marypha2lem1 8748 rankval4 9145 tcwf 9161 inlresf 9192 inrresf 9194 fin23lem16 9606 fin23lem29 9612 fin23lem30 9613 itunitc 9692 acncc 9711 wfgru 10087 renfdisj 10550 ioomax 12661 iccmax 12662 hashgval2 13587 fsumcom2 14962 fprodcom2 15171 dfphi2 15940 dmcoass 17155 letsr 17666 efgsf 18582 lssuni 19401 lpival 19707 psr1baslem 20036 cnsubdrglem 20278 retos 20444 istopon 21204 neips 21405 filssufilg 22203 xrhmeo 23233 iscmet3i 23598 ehlbase 23701 ovolge0 23765 unidmvol 23825 resinf1o 24801 divlogrlim 24899 dvloglem 24912 logf1o2 24914 atansssdm 25192 ppiub 25462 clwwlkn0 27488 sspval 28183 shintcli 28789 lnopco0i 29464 imaelshi 29518 nmopadjlem 29549 nmoptrii 29554 nmopcoi 29555 nmopcoadji 29561 idleop 29591 hmopidmchi 29611 hmopidmpji 29612 xrsclat 30333 rearchi 30561 dmvlsiga 30997 sxbrsigalem0 31138 dya2iocucvr 31151 eulerpartlemgh 31245 bnj110 31738 subfacp1lem1 32028 erdszelem2 32041 dfon2lem3 32632 trpredlem1 32669 frrlem6 32731 frrlem7 32732 filnetlem2 33330 taupi 34148 cnviun 39493 coiun1 39495 comptiunov2i 39549 cotrcltrcl 39568 cotrclrcl 39585 ssrab2f 40936 iooinlbub 41331 stirlinglem14 41928 sssalgen 42174 fvmptrabdm 43022 |
Copyright terms: Public domain | W3C validator |