New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 198 | . 2 |
3 | 2 | pm2.43i 43 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: ibir 233 elimh 922 elab3gf 2990 elimhyp 3710 elimhyp2v 3711 elimhyp3v 3712 elimhyp4v 3713 elpwi 3730 elpr2 3752 elpri 3753 elsni 3757 eltpi 3770 snssi 3852 prssi 3863 evennn 4506 oddnn 4507 evennnul 4508 oddnnul 4509 sucevenodd 4510 sucoddeven 4511 eventfin 4517 oddtfin 4518 nnadjoin 4520 nnadjoinpw 4521 elxpi 4800 elfunsi 5831 trd 5921 frd 5922 extd 5923 symd 5924 refd 5927 antid 5929 connexd 5931 elqsi 5978 pmfun 6015 elmapi 6016 cannc 6333 cantc 6336 |
Copyright terms: Public domain | W3C validator |