Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylnibr | Unicode version |
Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting an consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.) |
Ref | Expression |
---|---|
sylnibr.1 | |
sylnibr.2 |
Ref | Expression |
---|---|
sylnibr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylnibr.1 | . 2 | |
2 | sylnibr.2 | . . 3 | |
3 | 2 | bicomi 130 | . 2 |
4 | 1, 3 | sylnib 633 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 576 ax-in2 577 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: rexnalim 2359 nssr 3057 difdif 3097 unssin 3203 inssun 3204 undif3ss 3225 ssdif0im 3308 prneimg 3566 iundif2ss 3743 nssssr 3977 pofun 4067 frirrg 4105 regexmidlem1 4276 nndifsnid 6103 fidifsnid 6356 addnqprlemfl 6749 addnqprlemfu 6750 mulnqprlemfl 6765 mulnqprlemfu 6766 cauappcvgprlemladdru 6846 caucvgprprlemaddq 6898 fzpreddisj 9088 pw2dvdslemn 10543 |
Copyright terms: Public domain | W3C validator |