Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl5rbb | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5rbb.1 | |
syl5rbb.2 |
Ref | Expression |
---|---|
syl5rbb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5rbb.1 | . . 3 | |
2 | syl5rbb.2 | . . 3 | |
3 | 1, 2 | syl5bb 191 | . 2 |
4 | 3 | bicomd 140 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: syl5rbbr 194 pm5.17dc 874 dn1dc 929 csbabg 3031 uniiunlem 3155 inimasn 4926 cnvpom 5051 fnresdisj 5203 f1oiso 5695 reldm 6052 mptelixpg 6596 1idprl 7366 1idpru 7367 nndiv 8729 fzn 9790 fz1sbc 9844 metrest 12602 bj-indeq 13054 |
Copyright terms: Public domain | W3C validator |