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 3145 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓 |
3 | mprgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbir 232 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∈ wcel 2105 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 |
This theorem depends on definitions: df-bi 208 df-ral 3140 |
This theorem is referenced by: ss2rabi 4050 rabxm 4337 ssintub 4885 djussxp 5709 dmiin 5818 dfco2 6091 coiun 6102 tron 6207 onxpdisj 6303 wfrrel 7949 wfrdmss 7950 tfrlem6 8007 oawordeulem 8169 sbthlem1 8615 marypha2lem1 8887 rankval4 9284 tcwf 9300 inlresf 9331 inrresf 9333 fin23lem16 9745 fin23lem29 9751 fin23lem30 9752 itunitc 9831 acncc 9850 wfgru 10226 renfdisj 10689 ioomax 12799 iccmax 12800 hashgval2 13727 fsumcom2 15117 fprodcom2 15326 dfphi2 16099 dmcoass 17314 letsr 17825 efgsf 18784 lssuni 19640 lpival 19946 psr1baslem 20281 cnsubdrglem 20524 retos 20690 istopon 21448 neips 21649 filssufilg 22447 xrhmeo 23477 iscmet3i 23842 ehlbase 23945 ovolge0 24009 unidmvol 24069 resinf1o 25047 divlogrlim 25145 dvloglem 25158 logf1o2 25160 atansssdm 25438 ppiub 25707 clwwlkn0 27733 sspval 28427 shintcli 29033 lnopco0i 29708 imaelshi 29762 nmopadjlem 29793 nmoptrii 29798 nmopcoi 29799 nmopcoadji 29805 idleop 29835 hmopidmchi 29855 hmopidmpji 29856 xrsclat 30594 rearchi 30842 dmvlsiga 31287 sxbrsigalem0 31428 dya2iocucvr 31441 eulerpartlemgh 31535 bnj110 32029 subfacp1lem1 32323 erdszelem2 32336 dfon2lem3 32927 trpredlem1 32963 frrlem6 33025 frrlem7 33026 filnetlem2 33624 taupi 34486 cnviun 39873 coiun1 39875 comptiunov2i 39929 cotrcltrcl 39948 cotrclrcl 39965 ssrab2f 41260 iooinlbub 41652 stirlinglem14 42249 sssalgen 42495 fvmptrabdm 43369 smndex2dnrinv 44015 |
Copyright terms: Public domain | W3C validator |