![]() |
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 132 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylnib 676 |
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 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: rexnalim 2466 nssr 3215 difdif 3260 unssin 3374 inssun 3375 undif3ss 3396 ssdif0im 3487 dcun 3533 prneimg 3772 iundif2ss 3949 nssssr 4219 pofun 4309 frirrg 4347 regexmidlem1 4529 dcdifsnid 6499 unfidisj 6915 fidcenumlemrks 6946 difinfsn 7093 pw1nel3 7224 addnqprlemfl 7546 addnqprlemfu 7547 mulnqprlemfl 7562 mulnqprlemfu 7563 cauappcvgprlemladdru 7643 caucvgprprlemaddq 7695 fzpreddisj 10054 fprodntrivap 11573 pw2dvdslemn 12145 isnsgrp 12701 ivthinclemdisj 13778 pwtrufal 14396 pw1nct 14401 nninfsellemsuc 14410 |
Copyright terms: Public domain | W3C validator |