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 140 | . 2 |
4 | 1, 3 | syl5ib 153 | 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: syl5ibrcom 156 biimprd 157 nbn2 687 limelon 4371 eldifpw 4449 ssonuni 4459 onsucuni2 4535 peano2 4566 limom 4585 elrnmpt1 4849 cnveqb 5053 cnveq0 5054 relcoi1 5129 ndmfvg 5511 ffvresb 5642 caovord3d 6003 poxp 6191 nnm0r 6438 nnacl 6439 nnacom 6443 nnaass 6444 nndi 6445 nnmass 6446 nnmsucr 6447 nnmcom 6448 brecop 6582 ecopovtrn 6589 ecopovtrng 6592 elpm2r 6623 map0g 6645 fundmen 6763 mapxpen 6805 phpm 6822 f1vrnfibi 6901 elfir 6929 mulcmpblnq 7300 ordpipqqs 7306 mulcmpblnq0 7376 genpprecll 7446 genppreclu 7447 addcmpblnr 7671 ax1rid 7809 axpre-mulgt0 7819 cnegexlem1 8064 msqge0 8505 mulge0 8508 ltleap 8521 nnmulcl 8869 nnsub 8887 elnn0z 9195 ztri3or0 9224 nneoor 9284 uz11 9479 xltnegi 9762 frec2uzuzd 10327 seq3fveq2 10394 seq3shft2 10398 seq3split 10404 seq3caopr3 10406 seq3id2 10434 seq3homo 10435 m1expcl2 10467 expadd 10487 expmul 10490 faclbnd 10643 hashfzp1 10726 hashfacen 10735 seq3coll 10741 caucvgrelemcau 10908 recan 11037 rexanre 11148 fsumiun 11404 efexp 11609 dvdstr 11754 alzdvds 11777 zob 11813 gcdmultiplez 11939 dvdssq 11949 cncongr2 12015 prmdiveq 12147 pythagtriplem2 12177 pcexp 12220 elrestr 12506 restopn2 12730 txcn 12822 txlm 12826 isxms2 12999 bj-om 13660 bj-inf2vnlem2 13694 bj-inf2vn 13697 bj-inf2vn2 13698 |
Copyright terms: Public domain | W3C validator |