![]() |
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 677 |
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 615 ax-in2 616 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: rexnalim 2479 nssr 3230 difdif 3275 unssin 3389 inssun 3390 undif3ss 3411 ssdif0im 3502 dcun 3548 prneimg 3789 iundif2ss 3967 nssssr 4240 pofun 4330 frirrg 4368 regexmidlem1 4550 dcdifsnid 6530 unfidisj 6951 fidcenumlemrks 6983 difinfsn 7130 pw1nel3 7261 addnqprlemfl 7589 addnqprlemfu 7590 mulnqprlemfl 7605 mulnqprlemfu 7606 cauappcvgprlemladdru 7686 caucvgprprlemaddq 7738 fzpreddisj 10103 fprodntrivap 11627 pw2dvdslemn 12200 isnsgrp 12884 ivthinclemdisj 14595 lgseisenlem1 14928 pwtrufal 15226 pw1nct 15231 nninfsellemsuc 15240 |
Copyright terms: Public domain | W3C validator |