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 129 | . 2 |
4 | 1, 3 | syl5ib 143 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: syl5ibrcom 146 biimprd 147 nbn2 613 limelon 4136 eldifpw 4208 ssonuni 4214 onsucuni2 4288 peano2 4318 limom 4336 elrnmpt1 4585 cnveqb 4776 cnveq0 4777 relcoi1 4849 ndmfvg 5204 ffvresb 5328 caovord3d 5671 poxp 5853 nnm0r 6058 nnacl 6059 nnacom 6063 nnaass 6064 nndi 6065 nnmass 6066 nnmsucr 6067 nnmcom 6068 brecop 6196 ecopovtrn 6203 ecopovtrng 6206 fundmen 6286 phpm 6327 mulcmpblnq 6466 ordpipqqs 6472 mulcmpblnq0 6542 genpprecll 6612 genppreclu 6613 addcmpblnr 6824 ax1rid 6951 axpre-mulgt0 6961 cnegexlem1 7186 msqge0 7607 mulge0 7610 ltleap 7621 nnmulcl 7935 nnsub 7952 elnn0z 8258 ztri3or0 8287 nneoor 8340 uz11 8495 xltnegi 8748 frec2uzuzd 9188 iseqss 9226 iseqfveq2 9228 iseqshft2 9232 iseqsplit 9238 iseqcaopr3 9240 iseqhomo 9248 m1expcl2 9277 expadd 9297 expmul 9300 caucvgrelemcau 9579 recan 9705 bj-om 10061 peano5setOLD 10065 bj-inf2vnlem2 10096 bj-inf2vn 10099 bj-inf2vn2 10100 |
Copyright terms: Public domain | W3C validator |