![]() |
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: ![]() ![]() |
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 705 elab3gf 2902 elpwi 3599 elsni 3625 elpr2 3629 elpri 3630 eltpi 3654 snssi 3751 prssi 3765 eloni 4393 limuni2 4415 elxpi 4660 releldmb 4882 relelrnb 4883 elrnmpt2d 4900 elrelimasn 5012 funeu 5260 fneu 5339 fvelima 5588 eloprabi 6221 fo2ndf 6252 tfrlem9 6344 ecexr 6564 elqsi 6613 qsel 6638 ecopovsym 6657 ecopovsymg 6660 elpmi 6693 elmapi 6696 pmsspw 6709 brdomi 6775 en1uniel 6830 mapdom1g 6875 dif1en 6907 enomnilem 7166 omnimkv 7184 mkvprop 7186 fodjumkvlemres 7187 enmkvlem 7189 enwomnilem 7197 ltrnqi 7450 peano2nnnn 7882 peano2nn 8961 eliooord 9958 fzrev3i 10118 elfzole1 10185 elfzolt2 10186 bcp1nk 10774 rere 10906 climcl 11322 climcau 11387 fprodcnv 11665 isstruct2im 12522 restsspw 12754 mgmcl 12835 submss 12928 subm0cl 12930 submcl 12931 submmnd 12932 subgsubm 13135 istopfin 13960 uniopn 13961 iunopn 13962 inopn 13963 eltpsg 14000 basis1 14007 basis2 14008 eltg4i 14015 lmff 14209 psmetf 14285 psmet0 14287 psmettri2 14288 metflem 14309 xmetf 14310 xmeteq0 14319 xmettri2 14321 cncff 14524 cncfi 14525 limcresi 14595 dvcnp2cntop 14623 sinq34lt0t 14712 lgsdir2lem2 14891 2sqlem9 14932 |
Copyright terms: Public domain | W3C validator |