![]() |
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: ![]() ![]() |
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: bitr3di 194 pm5.17dc 890 dn1dc 945 csbabg 3066 uniiunlem 3190 inimasn 4964 cnvpom 5089 fnresdisj 5241 f1oiso 5735 reldm 6092 mptelixpg 6636 1idprl 7422 1idpru 7423 nndiv 8785 fzn 9853 fz1sbc 9907 metrest 12714 bj-indeq 13298 |
Copyright terms: Public domain | W3C validator |