![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6rbbr | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
syl6rbbr.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl6rbbr.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl6rbbr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6rbbr.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | syl6rbbr.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | bicomi 123 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl6rbb 186 |
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 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: imimorbdc 794 baib 827 pm5.6dc 834 xornbidc 1279 mo2dc 1952 reu8 2731 sbc6g 2782 r19.28m 3305 r19.45mv 3309 r19.27m 3310 ralsns 3399 rexsnsOLD 3401 iunconstm 3656 iinconstm 3657 unisucg 4117 funssres 4885 fncnv 4908 dff1o5 5078 funimass4 5167 fneqeql2 5219 fnniniseg2 5233 rexsupp 5234 unpreima 5235 dffo3 5257 funfvima 5333 dff13 5350 f1eqcocnv 5374 fliftf 5382 isocnv2 5395 eloprabga 5533 mpt22eqb 5552 opabex3d 5690 opabex3 5691 elxp6 5738 elxp7 5739 genpdflem 6490 ltexprlemloc 6581 xrlenlt 6881 negcon2 7060 elznn 8037 zq 8337 rpnegap 8390 |
Copyright terms: Public domain | W3C validator |