![]() |
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 | ibi.1 | . . 3 ⊢ (𝜑 → (𝜑 ↔ 𝜓)) | |
2 | 1 | biimpd 219 | . 2 ⊢ (𝜑 → (𝜑 → 𝜓)) |
3 | 2 | pm2.43i 52 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: ibir 257 elimh 1050 elab3gf 3388 elimhyp 4179 elimhyp2v 4180 elimhyp3v 4181 elimhyp4v 4182 elpwi 4201 elsni 4227 elpri 4230 eltpi 4261 snssi 4371 prssi 4385 prelpwi 4945 elxpi 5164 releldmb 5392 relelrnb 5393 elpredim 5730 eloni 5771 limuni2 5824 funeu 5951 fneu 6033 fvelima 6287 eloprabi 7277 fo2ndf 7329 tfrlem9 7526 oeeulem 7726 elqsi 7843 qsel 7869 ecopovsym 7892 elpmi 7918 elmapi 7921 pmsspw 7934 brdomi 8008 undom 8089 mapdom1 8166 ominf 8213 unblem2 8254 unfilem1 8265 fiin 8369 brwdomi 8514 canthwdom 8525 brwdom3i 8529 unxpwdom 8535 scott0 8787 acni 8906 pwcdadom 9076 fin1ai 9153 fin2i 9155 fin4i 9158 ssfin3ds 9190 fin23lem17 9198 fin23lem38 9209 fin23lem39 9210 isfin32i 9225 fin34 9250 isfin7-2 9256 fin1a2lem13 9272 fin12 9273 gchi 9484 wuntr 9565 wununi 9566 wunpw 9567 wunpr 9569 wun0 9578 tskpwss 9612 tskpw 9613 tsken 9614 grutr 9653 grupw 9655 grupr 9657 gruurn 9658 ingru 9675 indpi 9767 eliooord 12271 fzrev3i 12445 elfzole1 12517 elfzolt2 12518 fz1fzo0m1 12555 bcp1nk 13144 rere 13906 nn0abscl 14096 climcl 14274 rlimcl 14278 rlimdm 14326 o1res 14335 rlimdmo1 14392 climcau 14445 caucvgb 14454 fprodcnv 14757 cshws0 15855 restsspw 16139 mreiincl 16303 catidex 16382 catcocl 16393 catass 16394 homa1 16734 homahom2 16735 odulat 17192 dlatjmdi 17244 psrel 17250 psref2 17251 pstr2 17252 reldir 17280 dirdm 17281 dirref 17282 dirtr 17283 dirge 17284 mgmcl 17292 submss 17397 subm0cl 17399 submcl 17400 submmnd 17401 subgsubm 17663 symgbasf1o 17849 symginv 17868 psgneu 17972 odmulg 18019 efgsp1 18196 efgsres 18197 frgpnabl 18324 dprdgrp 18450 dprdf 18451 abvfge0 18870 abveq0 18874 abvmul 18877 abvtri 18878 lbsss 19125 lbssp 19127 lbsind 19128 opsrtoslem2 19533 opsrso 19535 domnchr 19928 cssi 20076 linds1 20197 linds2 20198 lindsind 20204 mdetunilem9 20474 uniopn 20750 iunopn 20751 inopn 20752 fiinopn 20754 eltpsg 20795 basis1 20802 basis2 20803 eltg4i 20812 lmff 21153 t1sep2 21221 cmpfii 21260 ptfinfin 21370 kqhmph 21670 fbasne0 21681 0nelfb 21682 fbsspw 21683 fbasssin 21687 ufli 21765 uffixfr 21774 elfm 21798 fclsopni 21866 fclselbas 21867 ustssxp 22055 ustbasel 22057 ustincl 22058 ustdiag 22059 ustinvel 22060 ustexhalf 22061 ustfilxp 22063 ustbas2 22076 ustbas 22078 psmetf 22158 psmet0 22160 psmettri2 22161 metflem 22180 xmetf 22181 xmeteq0 22190 xmettri2 22192 tmsxms 22338 tmsms 22339 metustsym 22407 tngnrg 22525 cncff 22743 cncfi 22744 cfili 23112 iscmet3lem2 23136 mbfres 23456 mbfimaopnlem 23467 limcresi 23694 dvcnp2 23728 ulmcl 24180 ulmf 24181 ulmcau 24194 pserulm 24221 pserdvlem2 24227 sinq34lt0t 24306 logtayl 24451 dchrmhm 25011 lgsdir2lem2 25096 2sqlem9 25197 mulog2sum 25271 eleei 25822 uhgrf 26002 ushgrf 26003 upgrf 26026 umgrf 26038 uspgrf 26094 usgrf 26095 usgrfs 26097 nbcplgr 26386 clwlkcompim 26732 tncp 27460 eulplig 27467 grpofo 27481 grpolidinv 27483 grpoass 27485 nvvop 27592 phpar 27807 pjch1 28657 toslub 29796 tosglb 29798 orngsqr 29932 zhmnrg 30139 issgon 30314 measfrge0 30394 measvnul 30397 measvun 30400 fzssfzo 30741 bnj916 31129 bnj983 31147 mfsdisj 31573 mtyf2 31574 maxsta 31577 mvtinf 31578 orderseqlem 31877 hfun 32410 hfsn 32411 hfelhf 32413 hfuni 32416 hfpw 32417 fneuni 32467 bj-elid 33215 mptsnunlem 33315 heibor1lem 33738 heiborlem1 33740 heiborlem3 33742 opidonOLD 33781 isexid2 33784 elrelsrelim 34378 elpcliN 35497 lnrfg 38006 pwinfi2 38184 frege55lem1c 38527 gneispacef 38750 gneispacef2 38751 gneispacern2 38754 gneispace0nelrn 38755 gneispaceel 38758 gneispacess 38760 trintALTVD 39430 trintALT 39431 eliuniin 39593 eliuniin2 39617 disjrnmpt2 39689 fvelimad 39772 stoweidlem35 40570 saluncl 40855 saldifcl 40857 0sal 40858 sge0resplit 40941 omedm 41034 afvelrnb0 41565 afvelima 41568 rlimdmafv 41578 submgmss 42117 submgmcl 42119 submgmmgm 42120 asslawass 42154 linindsi 42561 |
Copyright terms: Public domain | W3C validator |