![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ibi | Structured version Visualization version GIF version |
Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.) |
Ref | Expression |
---|---|
ibi.1 | ⊢ (𝜑 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ibi | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
2 | ibi.1 | . 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | mpbid 231 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 |
This theorem is referenced by: ibir 267 elab3gf 3634 elab3g 3635 elimhyp 4549 elimhyp2v 4550 elimhyp3v 4551 elimhyp4v 4552 elpwi 4565 elsni 4601 elpri 4606 eltpi 4646 snssi 4766 prssi 4779 snelpwi 5398 prelpwi 5402 elxpi 5653 releldmb 5899 relelrnb 5900 elrnmpt2d 5916 eloni 6325 limuni2 6377 funeu 6523 fneu 6609 fvelima 6905 fvelimad 6906 eloprabi 7991 fo2ndf 8049 orderseqlem 8085 tfrlem9 8327 oeeulem 8544 elqsi 8705 qsel 8731 ecopovsym 8754 elpmi 8780 elmapi 8783 pmsspw 8811 brdomi 8894 brdomiOLD 8895 en0 8953 en0r 8956 en1 8961 undomOLD 9000 mapdom1 9082 rexdif1en 9098 ominf 9198 ominfOLD 9199 unblem2 9236 unfilem1 9250 fiin 9354 brwdomi 9500 canthwdom 9511 brwdom3i 9515 unxpwdom 9521 scott0 9818 acni 9977 djuinf 10120 pwdjudom 10148 fin1ai 10225 fin2i 10227 fin4i 10230 ssfin3ds 10262 fin23lem17 10270 fin23lem38 10281 fin23lem39 10282 isfin32i 10297 fin34 10322 isfin7-2 10328 fin1a2lem13 10344 fin12 10345 gchi 10556 wuntr 10637 wununi 10638 wunpw 10639 wunpr 10641 wun0 10650 tskpwss 10684 tskpw 10685 tsken 10686 grutr 10725 grupw 10727 grupr 10729 gruurn 10730 ingru 10747 indpi 10839 eliooord 13315 fzrev3i 13500 elfzole1 13572 elfzolt2 13573 bcp1nk 14209 rere 14999 nn0abscl 15189 climcl 15373 rlimcl 15377 rlimdm 15425 o1res 15434 rlimdmo1 15492 climcau 15547 caucvgb 15556 fprodcnv 15858 cshws0 16966 restsspw 17305 mreiincl 17468 catidex 17546 catcocl 17557 catass 17558 homa1 17915 homahom2 17916 odulat 18316 dlatjmdi 18407 psrel 18450 psref2 18451 pstr2 18452 reldir 18480 dirdm 18481 dirref 18482 dirtr 18483 dirge 18484 mgmcl 18492 submss 18612 subm0cl 18614 submcl 18615 submmnd 18616 efmndbasf 18677 subgsubm 18941 symgbasf1o 19147 symginv 19175 psgneu 19279 odmulg 19329 frgpnabl 19644 dprdgrp 19775 dprdf 19776 abvfge0 20266 abveq0 20270 abvmul 20273 abvtri 20274 lbsss 20523 lbssp 20525 lbsind 20526 domnchr 20920 cssi 21073 linds1 21201 linds2 21202 lindsind 21208 opsrtoslem2 21447 opsrso 21449 mdetunilem9 21953 uniopn 22230 iunopn 22231 inopn 22232 fiinopn 22234 eltpsg 22276 eltpsgOLD 22277 basis1 22284 basis2 22285 eltg4i 22294 lmff 22636 t1sep2 22704 cmpfii 22744 ptfinfin 22854 kqhmph 23154 fbasne0 23165 0nelfb 23166 fbsspw 23167 fbasssin 23171 ufli 23249 uffixfr 23258 elfm 23282 fclsopni 23350 fclselbas 23351 ustssxp 23540 ustbasel 23542 ustincl 23543 ustdiag 23544 ustinvel 23545 ustexhalf 23546 ustfilxp 23548 ustbas2 23561 ustbas 23563 psmetf 23643 psmet0 23645 psmettri2 23646 metflem 23665 xmetf 23666 xmeteq0 23675 xmettri2 23677 tmsxms 23826 tmsms 23827 metustsym 23895 tngnrg 24022 cncff 24240 cncfi 24241 cfili 24616 iscmet3lem2 24640 mbfres 24992 mbfimaopnlem 25003 limcresi 25233 dvcnp2 25268 ulmcl 25724 ulmf 25725 ulmcau 25738 pserulm 25765 pserdvlem2 25771 sinq34lt0t 25850 logtayl 25999 dchrmhm 26573 lgsdir2lem2 26658 2sqlem9 26759 mulog2sum 26869 eleei 27732 uhgrf 27899 ushgrf 27900 upgrf 27923 umgrf 27935 uspgrf 27991 usgrf 27992 usgrfs 27994 nbcplgr 28268 clwlkcompim 28614 tncp 29306 eulplig 29313 grpofo 29327 grpolidinv 29329 grpoass 29331 nvvop 29437 phpar 29652 pjch1 30498 fzne1 31574 toslub 31716 tosglb 31718 orngsqr 31982 fldextsubrg 32217 fldextress 32218 zhmnrg 32417 issgon 32591 measfrge0 32671 measvnul 32674 measvun 32677 fzssfzo 33020 bnj916 33414 bnj983 33432 cplgredgex 33583 acycgrcycl 33610 mfsdisj 34013 mtyf2 34014 maxsta 34017 mvtinf 34018 hfun 34730 hfsn 34731 hfelhf 34733 hfuni 34736 hfpw 34737 fneuni 34786 curryset 35384 mptsnunlem 35776 heibor1lem 36235 heiborlem1 36237 heiborlem3 36239 opidonOLD 36278 isexid2 36281 elrelsrelim 36917 eqvrelqsel 37045 elpcliN 38323 lnrfg 41384 sdomne0 41627 sdomne0d 41628 pwinfi2 41776 frege55lem1c 42130 gneispacef 42349 gneispacef2 42350 gneispacern2 42353 gneispace0nelrn 42354 gneispaceel 42357 gneispacess 42359 mnuop123d 42484 trintALTVD 43104 trintALT 43105 eliuniin 43251 eliuniin2 43272 disjrnmpt2 43343 fvelima2 43424 stoweidlem35 44208 saluncl 44490 saldifcl 44492 0sal 44493 sge0resplit 44579 omedm 44672 funressneu 45213 afvelrnb0 45328 afvelima 45331 rlimdmafv 45341 funressndmafv2rn 45387 rlimdmafv2 45422 elsetpreimafv 45509 oexpnegALTV 45801 isisomgr 45948 submgmss 46018 submgmcl 46020 submgmmgm 46021 asslawass 46059 linindsi 46460 |
Copyright terms: Public domain | W3C validator |