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 142 | . 2 |
3 | 2 | pm2.43i 48 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: ibir 175 pm5.21nii 652 elab3gf 2743 elpwi 3391 elsni 3416 elpr2 3420 elpri 3421 eltpi 3439 snssi 3529 prssi 3543 eloni 4130 limuni2 4152 elxpi 4379 releldmb 4589 relelrnb 4590 funeu 4946 fneu 5023 fvelima 5246 eloprabi 5842 fo2ndf 5868 tfrlem9 5958 ecexr 6134 elqsi 6181 qsel 6206 ecopovsym 6225 ecopovsymg 6228 brdomi 6253 en1uniel 6307 dif1en 6364 ltrnqi 6611 peano2nnnn 7021 peano2nn 8051 eliooord 8951 fzrev3i 9105 elfzole1 9164 elfzolt2 9165 bcp1nk 9689 rere 9752 climcl 10121 climcau 10184 |
Copyright terms: Public domain | W3C validator |