| 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 234 | 1 ⊢ (𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 208 |
| 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 209 |
| This theorem is referenced by: ibir 270 elab3gf 3642 elab3g 3643 elimhyp 4543 elimhyp2v 4544 elimhyp3v 4545 elimhyp4v 4546 elpwi 4559 elsni 4596 elpri 4603 eltpi 4644 snssi 4741 prssi 4776 snelpwi 5408 prelpwi 5411 elxpi 5665 releldmb 5918 relelrnb 5919 elrnmpt2d 5938 eloni 6350 limuni2 6403 funeu 6540 fneu 6625 fvelima2 6913 fvelima 6926 fvelimad 6928 eloprabi 8038 fo2ndf 8093 orderseqlem 8130 tfrlem9 8349 oeeulem 8564 elqsi 8740 qsel 8771 ecopovsym 8794 elpmi 8820 elmapi 8823 pmsspw 8852 brdomi 8933 en0 8992 en0r 8994 en1 8998 mapdom1 9107 rexdif1en 9122 ominf 9201 unblem2 9230 unfilem1 9242 fodomfir 9265 fiin 9361 brwdomi 9509 canthwdom 9520 brwdom3i 9524 unxpwdom 9530 scott0 9837 acni 9994 djuinf 10138 pwdjudom 10164 fin1ai 10243 fin2i 10245 fin4i 10248 ssfin3ds 10280 fin23lem17 10288 fin23lem38 10299 fin23lem39 10300 isfin32i 10315 fin34 10340 isfin7-2 10346 fin1a2lem13 10362 fin12 10363 gchi 10575 wuntr 10656 wununi 10657 wunpw 10658 wunpr 10660 wun0 10669 tskpwss 10703 tskpw 10704 tsken 10705 grutr 10744 grupw 10746 grupr 10748 gruurn 10749 ingru 10766 indpi 10858 eliooord 13402 fzrev3i 13589 fzne1 13602 elfzole1 13666 elfzolt2 13667 bcp1nk 14323 rere 15139 nn0abscl 15329 climcl 15516 rlimcl 15520 rlimdm 15568 o1res 15577 rlimdmo1 15635 climcau 15688 caucvgb 15697 fprodcnv 16003 cshws0 17127 restsspw 17450 mreiincl 17614 catidex 17696 catcocl 17707 catass 17708 homa1 18060 homahom2 18061 odulat 18457 dlatjmdi 18548 psrel 18591 psref2 18592 pstr2 18593 reldir 18621 dirdm 18622 dirref 18623 dirtr 18624 dirge 18625 chnub 18644 mgmcl 18667 submgmss 18729 submgmcl 18731 submgmmgm 18732 submss 18833 subm0cl 18835 submcl 18836 submmnd 18837 efmndbasf 18899 subgsubm 19180 symgbasf1o 19405 symginv 19432 psgneu 19536 odmulg 19586 frgpnabl 19905 dprdgrp 20037 dprdf 20038 abvfge0 20850 abveq0 20854 abvmul 20857 abvtri 20858 orngsqr 20902 lbsss 21131 lbssp 21133 lbsind 21134 domnchr 21571 cssi 21723 linds1 21849 linds2 21850 lindsind 21856 opsrtoslem2 22096 opsrso 22098 mdetunilem9 22667 uniopn 22944 iunopn 22945 inopn 22946 fiinopn 22948 eltpsg 22990 basis1 22997 basis2 22998 eltg4i 23007 lmff 23348 t1sep2 23416 cmpfii 23456 ptfinfin 23566 kqhmph 23866 fbasne0 23877 0nelfb 23878 fbsspw 23879 fbasssin 23883 ufli 23961 uffixfr 23970 elfm 23994 fclsopni 24062 fclselbas 24063 ustssxp 24252 ustbasel 24254 ustincl 24255 ustdiag 24256 ustinvel 24257 ustexhalf 24258 ustfilxp 24260 ustbas2 24272 ustbas 24274 psmetf 24353 psmet0 24355 psmettri2 24356 metflem 24375 xmetf 24376 xmeteq0 24385 xmettri2 24387 tmsxms 24533 tmsms 24534 metustsym 24602 tngnrg 24721 cncff 24942 cncfi 24943 cfili 25317 iscmet3lem2 25341 mbfres 25693 mbfimaopnlem 25704 limcresi 25934 dvcnp2 25969 ulmcl 26431 ulmf 26432 ulmcau 26445 pserulm 26472 pserdvlem2 26478 sinq34lt0t 26561 logtayl 26712 dchrmhm 27292 lgsdir2lem2 27377 2sqlem9 27478 mulog2sum 27588 newbdayim 27983 eleei 29054 uhgrf 29219 ushgrf 29220 upgrf 29243 umgrf 29255 uspgrf 29311 usgrf 29312 usgrfs 29314 nbcplgr 29591 clwlkcompim 29936 tncp 30637 eulplig 30644 grpofo 30658 grpolidinv 30660 grpoass 30662 nvvop 30768 phpar 30983 pjch1 31829 nn0mnfxrd 32913 toslub 33111 tosglb 33113 suppgsumssiun 33212 exsslsb 33854 fldextsubrg 33906 fldextress 33908 zhmnrg 34222 issgon 34380 measfrge0 34460 measvnul 34463 measvun 34466 fzssfzo 34796 bnj916 35188 bnj983 35206 cplgredgex 35431 acycgrcycl 35457 mfsdisj 35860 mtyf2 35861 maxsta 35864 mvtinf 35865 r1peuqusdeg1 35953 hfun 36488 hfsn 36489 hfelhf 36491 hfuni 36494 hfpw 36495 fneuni 36667 elttcirr 36851 curryset 37391 mptsnunlem 37792 heibor1lem 38268 heiborlem1 38270 heiborlem3 38272 opidonOLD 38311 isexid2 38314 elrelsrelim 38902 presucmap 38954 eqvrelqsel 39159 eldisjsim1 39393 elpcliN 40477 lnrfg 43656 sdomne0 43949 sdomne0d 43950 pwinfi2 44098 frege55lem1c 44452 gneispacef 44671 gneispacef2 44672 gneispacern2 44675 gneispace0nelrn 44676 gneispaceel 44679 gneispacess 44681 mnuop123d 44798 trintALTVD 45415 trintALT 45416 eliuniin 45637 eliuniin2 45658 disjrnmpt2 45726 stoweidlem35 46569 saluncl 46851 saldifcl 46853 0sal 46854 sge0resplit 46940 omedm 47033 funressneu 47601 afvelrnb0 47718 afvelima 47721 rlimdmafv 47731 funressndmafv2rn 47777 rlimdmafv2 47812 elsetpreimafv 47951 oexpnegALTV 48259 gricbri 48498 grlimprop2 48568 grilcbri 48591 asslawass 48775 linindsi 49029 inisegn0a 49417 eloprab1st2nd 49449 uobrcl 49774 uobeq2 49982 isinito2 50080 basrestermcfolem 50152 discsnterm 50155 islmd 50246 |
| Copyright terms: Public domain | W3C validator |