| 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 231 | 1 ⊢ 𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 |
| This theorem depends on definitions: df-bi 207 df-ral 3062 |
| This theorem is referenced by: ss2rabi 4077 ssintub 4966 djussxp 5856 dmiin 5964 dfco2 6265 coiun 6276 tron 6407 onxpdisj 6510 epweon 7795 frrlem6 8316 frrlem7 8317 wfrrelOLD 8354 wfrdmssOLD 8355 tfrlem6 8422 oawordeulem 8592 sbthlem1 9123 marypha2lem1 9475 ttrclselem1 9765 rankval4 9907 tcwf 9923 inlresf 9954 inrresf 9956 fin23lem16 10375 fin23lem29 10381 fin23lem30 10382 itunitc 10461 acncc 10480 wfgru 10856 renfdisj 11321 ioomax 13462 iccmax 13463 hashgval2 14417 fsumcom2 15810 fprodcom2 16020 dfphi2 16811 oppccatf 17771 dmcoass 18111 letsr 18638 smndex2dnrinv 18928 efgsf 19747 lssuni 20937 lpival 21334 cnsubdrglem 21436 retos 21636 psr1baslem 22186 istopon 22918 neips 23121 filssufilg 23919 xrhmeo 24977 iscmet3i 25346 ehlbase 25449 ovolge0 25516 unidmvol 25576 resinf1o 26578 divlogrlim 26677 dvloglem 26690 logf1o2 26692 atansssdm 26976 ppiub 27248 bday1s 27876 lrrecse 27975 clwwlkn0 30047 sspval 30742 shintcli 31348 lnopco0i 32023 imaelshi 32077 nmopadjlem 32108 nmoptrii 32113 nmopcoi 32114 nmopcoadji 32120 idleop 32150 hmopidmchi 32170 hmopidmpji 32171 djussxp2 32658 xrsclat 33013 rearchi 33374 dmvlsiga 34130 sxbrsigalem0 34273 dya2iocucvr 34286 eulerpartlemgh 34380 bnj110 34872 subfacp1lem1 35184 erdszelem2 35197 dfon2lem3 35786 filnetlem2 36380 taupi 37324 cnviun 43663 coiun1 43665 comptiunov2i 43719 cotrcltrcl 43738 cotrclrcl 43755 ssrab2f 45122 iooinlbub 45514 stirlinglem14 46102 sssalgen 46350 fvmptrabdm 47305 stgr0 47927 unilbss 48737 |
| Copyright terms: Public domain | W3C validator |