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 694 elab3gf 2862 elpwi 3552 elsni 3578 elpr2 3582 elpri 3583 eltpi 3607 snssi 3701 prssi 3715 eloni 4336 limuni2 4358 elxpi 4603 releldmb 4824 relelrnb 4825 elrnmpt2d 4842 funeu 5196 fneu 5275 fvelima 5521 eloprabi 6145 fo2ndf 6175 tfrlem9 6267 ecexr 6486 elqsi 6533 qsel 6558 ecopovsym 6577 ecopovsymg 6580 elpmi 6613 elmapi 6616 pmsspw 6629 brdomi 6695 en1uniel 6750 mapdom1g 6793 dif1en 6825 enomnilem 7082 omnimkv 7100 mkvprop 7102 fodjumkvlemres 7103 enmkvlem 7105 enwomnilem 7113 ltrnqi 7342 peano2nnnn 7774 peano2nn 8846 eliooord 9833 fzrev3i 9991 elfzole1 10058 elfzolt2 10059 bcp1nk 10640 rere 10769 climcl 11183 climcau 11248 fprodcnv 11526 isstruct2im 12242 restsspw 12403 istopfin 12440 uniopn 12441 iunopn 12442 inopn 12443 eltpsg 12480 basis1 12487 basis2 12488 eltg4i 12497 lmff 12691 psmetf 12767 psmet0 12769 psmettri2 12770 metflem 12791 xmetf 12792 xmeteq0 12801 xmettri2 12803 cncff 13006 cncfi 13007 limcresi 13077 dvcnp2cntop 13105 sinq34lt0t 13194 |
Copyright terms: Public domain | W3C validator |