| 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 232 | 1 ⊢ (𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: ibir 268 elab3gf 3684 elab3g 3685 elimhyp 4591 elimhyp2v 4592 elimhyp3v 4593 elimhyp4v 4594 elpwi 4607 elsni 4643 elpri 4649 eltpi 4688 snssi 4808 prssi 4821 snelpwi 5448 prelpwi 5452 elxpi 5707 releldmb 5957 relelrnb 5958 elrnmpt2d 5977 eloni 6394 limuni2 6446 funeu 6591 fneu 6678 fvelima2 6961 fvelima 6974 fvelimad 6976 eloprabi 8088 fo2ndf 8146 orderseqlem 8182 tfrlem9 8425 oeeulem 8639 elqsi 8810 qsel 8836 ecopovsym 8859 elpmi 8886 elmapi 8889 pmsspw 8917 brdomi 8999 brdomiOLD 9000 en0 9058 en0r 9060 en1 9064 undomOLD 9100 mapdom1 9182 rexdif1en 9198 ominf 9294 ominfOLD 9295 unblem2 9329 unfilem1 9343 fodomfir 9368 fiin 9462 brwdomi 9608 canthwdom 9619 brwdom3i 9623 unxpwdom 9629 scott0 9926 acni 10085 djuinf 10229 pwdjudom 10255 fin1ai 10333 fin2i 10335 fin4i 10338 ssfin3ds 10370 fin23lem17 10378 fin23lem38 10389 fin23lem39 10390 isfin32i 10405 fin34 10430 isfin7-2 10436 fin1a2lem13 10452 fin12 10453 gchi 10664 wuntr 10745 wununi 10746 wunpw 10747 wunpr 10749 wun0 10758 tskpwss 10792 tskpw 10793 tsken 10794 grutr 10833 grupw 10835 grupr 10837 gruurn 10838 ingru 10855 indpi 10947 eliooord 13446 fzrev3i 13631 fzne1 13644 elfzole1 13707 elfzolt2 13708 bcp1nk 14356 rere 15161 nn0abscl 15351 climcl 15535 rlimcl 15539 rlimdm 15587 o1res 15596 rlimdmo1 15654 climcau 15707 caucvgb 15716 fprodcnv 16019 cshws0 17139 restsspw 17476 mreiincl 17639 catidex 17717 catcocl 17728 catass 17729 homa1 18082 homahom2 18083 odulat 18480 dlatjmdi 18571 psrel 18614 psref2 18615 pstr2 18616 reldir 18644 dirdm 18645 dirref 18646 dirtr 18647 dirge 18648 mgmcl 18656 submgmss 18718 submgmcl 18720 submgmmgm 18721 submss 18822 subm0cl 18824 submcl 18825 submmnd 18826 efmndbasf 18888 subgsubm 19166 symgbasf1o 19392 symginv 19420 psgneu 19524 odmulg 19574 frgpnabl 19893 dprdgrp 20025 dprdf 20026 abvfge0 20815 abveq0 20819 abvmul 20822 abvtri 20823 lbsss 21076 lbssp 21078 lbsind 21079 domnchr 21547 cssi 21702 linds1 21830 linds2 21831 lindsind 21837 opsrtoslem2 22080 opsrso 22082 mdetunilem9 22626 uniopn 22903 iunopn 22904 inopn 22905 fiinopn 22907 eltpsg 22949 eltpsgOLD 22950 basis1 22957 basis2 22958 eltg4i 22967 lmff 23309 t1sep2 23377 cmpfii 23417 ptfinfin 23527 kqhmph 23827 fbasne0 23838 0nelfb 23839 fbsspw 23840 fbasssin 23844 ufli 23922 uffixfr 23931 elfm 23955 fclsopni 24023 fclselbas 24024 ustssxp 24213 ustbasel 24215 ustincl 24216 ustdiag 24217 ustinvel 24218 ustexhalf 24219 ustfilxp 24221 ustbas2 24234 ustbas 24236 psmetf 24316 psmet0 24318 psmettri2 24319 metflem 24338 xmetf 24339 xmeteq0 24348 xmettri2 24350 tmsxms 24499 tmsms 24500 metustsym 24568 tngnrg 24695 cncff 24919 cncfi 24920 cfili 25302 iscmet3lem2 25326 mbfres 25679 mbfimaopnlem 25690 limcresi 25920 dvcnp2 25955 dvcnp2OLD 25956 ulmcl 26424 ulmf 26425 ulmcau 26438 pserulm 26465 pserdvlem2 26472 sinq34lt0t 26551 logtayl 26702 dchrmhm 27285 lgsdir2lem2 27370 2sqlem9 27471 mulog2sum 27581 eleei 28912 uhgrf 29079 ushgrf 29080 upgrf 29103 umgrf 29115 uspgrf 29171 usgrf 29172 usgrfs 29174 nbcplgr 29451 clwlkcompim 29800 tncp 30497 eulplig 30504 grpofo 30518 grpolidinv 30520 grpoass 30522 nvvop 30628 phpar 30843 pjch1 31689 toslub 32963 tosglb 32965 chnub 33002 orngsqr 33334 exsslsb 33647 fldextsubrg 33702 fldextress 33703 zhmnrg 33966 issgon 34124 measfrge0 34204 measvnul 34207 measvun 34210 fzssfzo 34554 bnj916 34947 bnj983 34965 cplgredgex 35126 acycgrcycl 35152 mfsdisj 35555 mtyf2 35556 maxsta 35559 mvtinf 35560 r1peuqusdeg1 35648 hfun 36179 hfsn 36180 hfelhf 36182 hfuni 36185 hfpw 36186 fneuni 36348 curryset 36947 mptsnunlem 37339 heibor1lem 37816 heiborlem1 37818 heiborlem3 37820 opidonOLD 37859 isexid2 37862 elrelsrelim 38489 eqvrelqsel 38617 elpcliN 39895 lnrfg 43131 sdomne0 43426 sdomne0d 43427 pwinfi2 43575 frege55lem1c 43929 gneispacef 44148 gneispacef2 44149 gneispacern2 44152 gneispace0nelrn 44153 gneispaceel 44156 gneispacess 44158 mnuop123d 44281 trintALTVD 44900 trintALT 44901 eliuniin 45104 eliuniin2 45125 disjrnmpt2 45193 stoweidlem35 46050 saluncl 46332 saldifcl 46334 0sal 46335 sge0resplit 46421 omedm 46514 funressneu 47059 afvelrnb0 47176 afvelima 47179 rlimdmafv 47189 funressndmafv2rn 47235 rlimdmafv2 47270 elsetpreimafv 47372 oexpnegALTV 47664 gricbri 47885 grlimprop2 47953 grilcbri 47969 asslawass 48109 linindsi 48364 |
| Copyright terms: Public domain | W3C validator |