Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ibi | Unicode 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 144 | . 2 |
3 | 2 | pm2.43i 49 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: ibir 177 pm5.21nii 704 elab3gf 2885 elpwi 3581 elsni 3607 elpr2 3611 elpri 3612 eltpi 3636 snssi 3733 prssi 3747 eloni 4369 limuni2 4391 elxpi 4636 releldmb 4857 relelrnb 4858 elrnmpt2d 4875 funeu 5233 fneu 5312 fvelima 5559 eloprabi 6187 fo2ndf 6218 tfrlem9 6310 ecexr 6530 elqsi 6577 qsel 6602 ecopovsym 6621 ecopovsymg 6624 elpmi 6657 elmapi 6660 pmsspw 6673 brdomi 6739 en1uniel 6794 mapdom1g 6837 dif1en 6869 enomnilem 7126 omnimkv 7144 mkvprop 7146 fodjumkvlemres 7147 enmkvlem 7149 enwomnilem 7157 ltrnqi 7395 peano2nnnn 7827 peano2nn 8902 eliooord 9897 fzrev3i 10056 elfzole1 10123 elfzolt2 10124 bcp1nk 10708 rere 10841 climcl 11257 climcau 11322 fprodcnv 11600 isstruct2im 12438 restsspw 12619 mgmcl 12643 submss 12728 subm0cl 12730 submcl 12731 istopfin 12991 uniopn 12992 iunopn 12993 inopn 12994 eltpsg 13031 basis1 13038 basis2 13039 eltg4i 13048 lmff 13242 psmetf 13318 psmet0 13320 psmettri2 13321 metflem 13342 xmetf 13343 xmeteq0 13352 xmettri2 13354 cncff 13557 cncfi 13558 limcresi 13628 dvcnp2cntop 13656 sinq34lt0t 13745 lgsdir2lem2 13923 2sqlem9 13953 |
Copyright terms: Public domain | W3C validator |