Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl5ib | Unicode version |
Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5ib.1 | |
syl5ib.2 |
Ref | Expression |
---|---|
syl5ib |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5ib.1 | . 2 | |
2 | syl5ib.2 | . . 3 | |
3 | 2 | biimpd 143 | . 2 |
4 | 1, 3 | syl5 32 | 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 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: syl5ibcom 154 syl5ibr 155 sbft 1841 gencl 2762 spsbc 2966 prexg 4196 posng 4683 sosng 4684 optocl 4687 relcnvexb 5150 funimass1 5275 dmfex 5387 f1ocnvb 5456 eqfnfv2 5594 elpreima 5615 dff13 5747 f1ocnvfv 5758 f1ocnvfvb 5759 fliftfun 5775 eusvobj2 5839 mpoxopn0yelv 6218 rntpos 6236 erexb 6538 findcard2 6867 findcard2s 6868 xpfi 6907 sbthlemi3 6936 enq0tr 7396 addnqprllem 7489 addnqprulem 7490 distrlem1prl 7544 distrlem1pru 7545 recexprlem1ssl 7595 recexprlem1ssu 7596 elrealeu 7791 addcan 8099 addcan2 8100 neg11 8170 negreb 8184 mulcanapd 8579 receuap 8587 cju 8877 nn1suc 8897 nnaddcl 8898 nndivtr 8920 znegclb 9245 zaddcllempos 9249 zmulcl 9265 zeo 9317 uz11 9509 uzp1 9520 eqreznegel 9573 xneg11 9791 xnegdi 9825 modqadd1 10317 modqmul1 10333 frec2uzltd 10359 bccmpl 10688 fz1eqb 10725 cj11 10869 rennim 10966 resqrexlemgt0 10984 efne0 11641 dvdsabseq 11807 pcfac 12302 grpinveu 12741 uptx 13068 hmeocnvb 13112 tgioo 13340 bj-nnbidc 13792 bj-prexg 13946 strcollnft 14019 |
Copyright terms: Public domain | W3C validator |