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 1355 sbal2 1975 eqsnm 3652 fnressn 5574 fressnfv 5575 eluniimadm 5634 genpassl 7300 genpassu 7301 1idprl 7366 1idpru 7367 axcaucvglemres 7675 negeq0 7984 muleqadd 8396 crap0 8680 addltmul 8914 fzrev 9819 modq0 10057 cjap0 10634 cjne0 10635 caucvgrelemrec 10706 lenegsq 10822 isumss 11115 fsumsplit 11131 sumsplitdc 11156 dvdsabseq 11457 oddennn 11816 metrest 12586 elabgf0 12880 |
Copyright terms: Public domain | W3C validator |