![]() |
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 143 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | pm2.43i 49 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ibir 176 pm5.21nii 656 elab3gf 2766 elpwi 3442 elsni 3468 elpr2 3472 elpri 3473 eltpi 3493 snssi 3587 prssi 3601 eloni 4211 limuni2 4233 elxpi 4468 releldmb 4685 relelrnb 4686 funeu 5053 fneu 5131 fvelima 5369 eloprabi 5980 fo2ndf 6006 tfrlem9 6098 ecexr 6311 elqsi 6358 qsel 6383 ecopovsym 6402 ecopovsymg 6405 elpmi 6438 elmapi 6441 pmsspw 6454 brdomi 6520 en1uniel 6575 mapdom1g 6617 dif1en 6649 enomnilem 6855 ltrnqi 7041 peano2nnnn 7451 peano2nn 8495 eliooord 9407 fzrev3i 9563 elfzole1 9627 elfzolt2 9628 bcp1nk 10231 rere 10360 climcl 10731 climcau 10797 isstruct2im 11565 restsspw 11723 istopfin 11760 uniopn 11761 iunopn 11762 inopn 11763 eltpsg 11799 basis1 11806 basis2 11807 eltg4i 11816 cncff 11906 cncfi 11907 |
Copyright terms: Public domain | W3C validator |