![]() |
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 3671 elab3g 3672 elimhyp 4588 elimhyp2v 4589 elimhyp3v 4590 elimhyp4v 4591 elpwi 4604 elsni 4640 elpri 4646 eltpi 4686 snssi 4807 prssi 4820 snelpwi 5441 prelpwi 5445 elxpi 5696 releldmb 5944 relelrnb 5945 elrnmpt2d 5962 eloni 6378 limuni2 6430 funeu 6576 fneu 6662 fvelima 6960 fvelimad 6962 eloprabi 8069 fo2ndf 8127 orderseqlem 8163 tfrlem9 8407 oeeulem 8623 elqsi 8791 qsel 8817 ecopovsym 8840 elpmi 8867 elmapi 8870 pmsspw 8898 brdomi 8981 brdomiOLD 8982 en0 9041 en0r 9044 en1 9049 undomOLD 9090 mapdom1 9172 rexdif1en 9188 ominf 9285 ominfOLD 9286 unblem2 9323 unfilem1 9337 fodomfir 9363 fiin 9458 brwdomi 9604 canthwdom 9615 brwdom3i 9619 unxpwdom 9625 scott0 9922 acni 10081 djuinf 10224 pwdjudom 10250 fin1ai 10327 fin2i 10329 fin4i 10332 ssfin3ds 10364 fin23lem17 10372 fin23lem38 10383 fin23lem39 10384 isfin32i 10399 fin34 10424 isfin7-2 10430 fin1a2lem13 10446 fin12 10447 gchi 10658 wuntr 10739 wununi 10740 wunpw 10741 wunpr 10743 wun0 10752 tskpwss 10786 tskpw 10787 tsken 10788 grutr 10827 grupw 10829 grupr 10831 gruurn 10832 ingru 10849 indpi 10941 eliooord 13431 fzrev3i 13616 elfzole1 13688 elfzolt2 13689 bcp1nk 14329 rere 15122 nn0abscl 15312 climcl 15496 rlimcl 15500 rlimdm 15548 o1res 15557 rlimdmo1 15615 climcau 15670 caucvgb 15679 fprodcnv 15980 cshws0 17099 restsspw 17441 mreiincl 17604 catidex 17682 catcocl 17693 catass 17694 homa1 18054 homahom2 18055 odulat 18455 dlatjmdi 18546 psrel 18589 psref2 18590 pstr2 18591 reldir 18619 dirdm 18620 dirref 18621 dirtr 18622 dirge 18623 mgmcl 18631 submgmss 18693 submgmcl 18695 submgmmgm 18696 submss 18794 subm0cl 18796 submcl 18797 submmnd 18798 efmndbasf 18860 subgsubm 19138 symgbasf1o 19368 symginv 19396 psgneu 19500 odmulg 19550 frgpnabl 19869 dprdgrp 20001 dprdf 20002 abvfge0 20789 abveq0 20793 abvmul 20796 abvtri 20797 lbsss 21051 lbssp 21053 lbsind 21054 domnchr 21522 cssi 21676 linds1 21804 linds2 21805 lindsind 21811 opsrtoslem2 22065 opsrso 22067 mdetunilem9 22610 uniopn 22887 iunopn 22888 inopn 22889 fiinopn 22891 eltpsg 22933 eltpsgOLD 22934 basis1 22941 basis2 22942 eltg4i 22951 lmff 23293 t1sep2 23361 cmpfii 23401 ptfinfin 23511 kqhmph 23811 fbasne0 23822 0nelfb 23823 fbsspw 23824 fbasssin 23828 ufli 23906 uffixfr 23915 elfm 23939 fclsopni 24007 fclselbas 24008 ustssxp 24197 ustbasel 24199 ustincl 24200 ustdiag 24201 ustinvel 24202 ustexhalf 24203 ustfilxp 24205 ustbas2 24218 ustbas 24220 psmetf 24300 psmet0 24302 psmettri2 24303 metflem 24322 xmetf 24323 xmeteq0 24332 xmettri2 24334 tmsxms 24483 tmsms 24484 metustsym 24552 tngnrg 24679 cncff 24901 cncfi 24902 cfili 25284 iscmet3lem2 25308 mbfres 25661 mbfimaopnlem 25672 limcresi 25902 dvcnp2 25937 dvcnp2OLD 25938 ulmcl 26407 ulmf 26408 ulmcau 26421 pserulm 26448 pserdvlem2 26455 sinq34lt0t 26534 logtayl 26684 dchrmhm 27267 lgsdir2lem2 27352 2sqlem9 27453 mulog2sum 27563 eleei 28828 uhgrf 28995 ushgrf 28996 upgrf 29019 umgrf 29031 uspgrf 29087 usgrf 29088 usgrfs 29090 nbcplgr 29367 clwlkcompim 29714 tncp 30408 eulplig 30415 grpofo 30429 grpolidinv 30431 grpoass 30433 nvvop 30539 phpar 30754 pjch1 31600 fzne1 32693 toslub 32846 tosglb 32848 chnub 32884 orngsqr 33187 fldextsubrg 33546 fldextress 33547 zhmnrg 33795 issgon 33969 measfrge0 34049 measvnul 34052 measvun 34055 fzssfzo 34398 bnj916 34791 bnj983 34809 cplgredgex 34961 acycgrcycl 34988 mfsdisj 35391 mtyf2 35392 maxsta 35395 mvtinf 35396 r1peuqusdeg1 35484 hfun 36015 hfsn 36016 hfelhf 36018 hfuni 36021 hfpw 36022 fneuni 36072 curryset 36666 mptsnunlem 37058 heibor1lem 37523 heiborlem1 37525 heiborlem3 37527 opidonOLD 37566 isexid2 37569 elrelsrelim 38199 eqvrelqsel 38327 elpcliN 39605 lnrfg 42817 sdomne0 43117 sdomne0d 43118 pwinfi2 43266 frege55lem1c 43620 gneispacef 43839 gneispacef2 43840 gneispacern2 43843 gneispace0nelrn 43844 gneispaceel 43847 gneispacess 43849 mnuop123d 43973 trintALTVD 44593 trintALT 44594 eliuniin 44737 eliuniin2 44758 disjrnmpt2 44831 fvelima2 44905 stoweidlem35 45692 saluncl 45974 saldifcl 45976 0sal 45977 sge0resplit 46063 omedm 46156 funressneu 46698 afvelrnb0 46813 afvelima 46816 rlimdmafv 46826 funressndmafv2rn 46872 rlimdmafv2 46907 elsetpreimafv 46993 oexpnegALTV 47285 gricbri 47500 grlimprop2 47528 grilcbri 47535 asslawass 47606 linindsi 47866 |
Copyright terms: Public domain | W3C validator |