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 181 | . 2 |
4 | 3 | bicomd 129 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 |
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: syl5rbbr 184 pm5.17dc 810 dn1dc 867 csbabg 2907 uniiunlem 3028 inimasn 4741 cnvpom 4860 fnresdisj 5009 f1oiso 5465 reldm 5812 1idprl 6688 1idpru 6689 nndiv 7954 fzn 8906 fz1sbc 8958 bj-indeq 10053 |
Copyright terms: Public domain | W3C validator |