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 2922 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓 |
3 | mprgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbir 221 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∈ wcel 1990 ∀wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 |
This theorem depends on definitions: df-bi 197 df-ral 2917 |
This theorem is referenced by: ss2rabi 3684 rabxm 3961 ssintub 4495 djussxp 5267 dmiin 5369 dfco2 5634 coiun 5645 tron 5746 onxpdisj 5847 wfrrel 7420 wfrdmss 7421 tfrlem6 7478 oawordeulem 7634 sbthlem1 8070 marypha2lem1 8341 rankval4 8730 tcwf 8746 fin23lem16 9157 fin23lem29 9163 fin23lem30 9164 itunitc 9243 acncc 9262 wfgru 9638 renfdisj 10098 ioomax 12248 iccmax 12249 hashgval2 13167 fsumcom2 14505 fsumcom2OLD 14506 fprodcom2 14714 fprodcom2OLD 14715 dfphi2 15479 dmcoass 16716 letsr 17227 efgsf 18142 lssuni 18940 lpival 19245 psr1baslem 19555 cnsubdrglem 19797 retos 19964 istopon 20717 neips 20917 filssufilg 21715 xrhmeo 22745 iscmet3i 23110 ehlbase 23194 ovolge0 23249 unidmvol 23309 resinf1o 24282 divlogrlim 24381 dvloglem 24394 logf1o2 24396 atansssdm 24660 ppiub 24929 sspval 27578 shintcli 28188 lnopco0i 28863 imaelshi 28917 nmopadjlem 28948 nmoptrii 28953 nmopcoi 28954 nmopcoadji 28960 idleop 28990 hmopidmchi 29010 hmopidmpji 29011 xrsclat 29680 rearchi 29842 dmvlsiga 30192 sxbrsigalem0 30333 dya2iocucvr 30346 eulerpartlemgh 30440 bnj110 30928 subfacp1lem1 31161 erdszelem2 31174 dfon2lem3 31690 trpredlem1 31727 frrlem6 31789 frrlem7 31790 filnetlem2 32374 taupi 33169 cnviun 37942 coiun1 37944 comptiunov2i 37998 cotrcltrcl 38017 cotrclrcl 38034 ssrab2f 39300 iooinlbub 39723 stirlinglem14 40304 sssalgen 40553 |
Copyright terms: Public domain | W3C validator |