Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6rbbr | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
syl6rbbr.1 | |
syl6rbbr.2 |
Ref | Expression |
---|---|
syl6rbbr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6rbbr.1 | . 2 | |
2 | syl6rbbr.2 | . . 3 | |
3 | 2 | bicomi 131 | . 2 |
4 | 1, 3 | syl6rbb 196 | 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: imimorbdc 866 baib 889 pm5.6dc 896 xornbidc 1354 mo2dc 2032 reu8 2853 sbc6g 2906 dfss4st 3279 r19.28m 3422 r19.45mv 3426 r19.44mv 3427 r19.27m 3428 ralsnsg 3531 ralsns 3532 iunconstm 3791 iinconstm 3792 exmidsssnc 4096 unisucg 4306 relsng 4612 funssres 5135 fncnv 5159 dff1o5 5344 funimass4 5440 fneqeql2 5497 fnniniseg2 5511 rexsupp 5512 unpreima 5513 dffo3 5535 funfvima 5617 dff13 5637 f1eqcocnv 5660 fliftf 5668 isocnv2 5681 eloprabga 5826 mpo2eqb 5848 opabex3d 5987 opabex3 5988 elxp6 6035 elxp7 6036 sbthlemi5 6817 sbthlemi6 6818 genpdflem 7283 ltnqpr 7369 ltexprlemloc 7383 xrlenlt 7797 negcon2 7983 dfinfre 8682 sup3exmid 8683 elznn 9038 zq 9386 rpnegap 9442 modqmuladdnn0 10109 shftdm 10562 rexfiuz 10729 rexanuz2 10731 sumsplitdc 11169 fsum2dlemstep 11171 odd2np1 11497 divalgb 11549 infssuzex 11569 isprm4 11727 ctiunctlemudc 11877 tx1cn 12365 tx2cn 12366 cnbl0 12630 cnblcld 12631 reopnap 12634 pilem1 12787 sinq34lt0t 12839 |
Copyright terms: Public domain | W3C validator |