Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl5rbbr | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
syl5rbbr.1 | |
syl5rbbr.2 |
Ref | Expression |
---|---|
syl5rbbr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5rbbr.1 | . . 3 | |
2 | 1 | bicomi 131 | . 2 |
3 | syl5rbbr.2 | . 2 | |
4 | 2, 3 | syl5rbb 192 | 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: xordc 1370 sbal2 1995 eqsnm 3677 fnressn 5599 fressnfv 5600 eluniimadm 5659 genpassl 7325 genpassu 7326 1idprl 7391 1idpru 7392 axcaucvglemres 7700 negeq0 8009 muleqadd 8422 crap0 8709 addltmul 8949 fzrev 9857 modq0 10095 cjap0 10672 cjne0 10673 caucvgrelemrec 10744 lenegsq 10860 isumss 11153 fsumsplit 11169 sumsplitdc 11194 dvdsabseq 11534 oddennn 11894 metrest 12664 elabgf0 12973 |
Copyright terms: Public domain | W3C validator |