Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl5ibr | Unicode version |
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) (Revised by NM, 22-Sep-2013.) |
Ref | Expression |
---|---|
syl5ibr.1 | |
syl5ibr.2 |
Ref | Expression |
---|---|
syl5ibr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5ibr.1 | . 2 | |
2 | syl5ibr.2 | . . 3 | |
3 | 2 | bicomd 139 | . 2 |
4 | 1, 3 | syl5ib 152 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: syl5ibrcom 155 biimprd 156 nbn2 645 limelon 4154 eldifpw 4226 ssonuni 4232 onsucuni2 4307 peano2 4336 limom 4354 elrnmpt1 4603 cnveqb 4796 cnveq0 4797 relcoi1 4869 ndmfvg 5225 ffvresb 5349 caovord3d 5691 poxp 5873 nnm0r 6081 nnacl 6082 nnacom 6086 nnaass 6087 nndi 6088 nnmass 6089 nnmsucr 6090 nnmcom 6091 brecop 6219 ecopovtrn 6226 ecopovtrng 6229 fundmen 6309 phpm 6351 f1vrnfibi 6394 mulcmpblnq 6558 ordpipqqs 6564 mulcmpblnq0 6634 genpprecll 6704 genppreclu 6705 addcmpblnr 6916 ax1rid 7043 axpre-mulgt0 7053 cnegexlem1 7283 msqge0 7716 mulge0 7719 ltleap 7730 nnmulcl 8060 nnsub 8077 elnn0z 8364 ztri3or0 8393 nneoor 8449 uz11 8641 xltnegi 8902 frec2uzuzd 9404 iseqss 9446 iseqfveq2 9448 iseqshft2 9452 iseqsplit 9458 iseqcaopr3 9460 iseqhomo 9468 m1expcl2 9498 expadd 9518 expmul 9521 faclbnd 9668 caucvgrelemcau 9866 recan 9995 rexanre 10106 dvdstr 10232 alzdvds 10254 zob 10291 gcdmultiplez 10410 dvdssq 10420 cncongr2 10486 bj-om 10732 bj-inf2vnlem2 10766 bj-inf2vn 10769 bj-inf2vn2 10770 |
Copyright terms: Public domain | W3C validator |