![]() |
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 131 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylnib 648 |
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 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: rexnalim 2401 nssr 3123 difdif 3167 unssin 3281 inssun 3282 undif3ss 3303 ssdif0im 3393 dcun 3439 prneimg 3667 iundif2ss 3844 nssssr 4104 pofun 4194 frirrg 4232 regexmidlem1 4408 dcdifsnid 6354 unfidisj 6763 fidcenumlemrks 6793 difinfsn 6937 addnqprlemfl 7315 addnqprlemfu 7316 mulnqprlemfl 7331 mulnqprlemfu 7332 cauappcvgprlemladdru 7412 caucvgprprlemaddq 7464 fzpreddisj 9744 pw2dvdslemn 11688 pwtrufal 12884 nninfsellemsuc 12900 |
Copyright terms: Public domain | W3C validator |