Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ibi | 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 143 | . 2 ⊢ (𝜑 → (𝜑 → 𝜓)) |
3 | 2 | pm2.43i 49 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ibir 176 pm5.21nii 699 elab3gf 2880 elpwi 3575 elsni 3601 elpr2 3605 elpri 3606 eltpi 3630 snssi 3724 prssi 3738 eloni 4360 limuni2 4382 elxpi 4627 releldmb 4848 relelrnb 4849 elrnmpt2d 4866 funeu 5223 fneu 5302 fvelima 5548 eloprabi 6175 fo2ndf 6206 tfrlem9 6298 ecexr 6518 elqsi 6565 qsel 6590 ecopovsym 6609 ecopovsymg 6612 elpmi 6645 elmapi 6648 pmsspw 6661 brdomi 6727 en1uniel 6782 mapdom1g 6825 dif1en 6857 enomnilem 7114 omnimkv 7132 mkvprop 7134 fodjumkvlemres 7135 enmkvlem 7137 enwomnilem 7145 ltrnqi 7383 peano2nnnn 7815 peano2nn 8890 eliooord 9885 fzrev3i 10044 elfzole1 10111 elfzolt2 10112 bcp1nk 10696 rere 10829 climcl 11245 climcau 11310 fprodcnv 11588 isstruct2im 12426 restsspw 12589 mgmcl 12613 submss 12698 subm0cl 12700 submcl 12701 istopfin 12792 uniopn 12793 iunopn 12794 inopn 12795 eltpsg 12832 basis1 12839 basis2 12840 eltg4i 12849 lmff 13043 psmetf 13119 psmet0 13121 psmettri2 13122 metflem 13143 xmetf 13144 xmeteq0 13153 xmettri2 13155 cncff 13358 cncfi 13359 limcresi 13429 dvcnp2cntop 13457 sinq34lt0t 13546 lgsdir2lem2 13724 2sqlem9 13754 |
Copyright terms: Public domain | W3C validator |