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 1804 gencl 2692 spsbc 2893 prexg 4103 posng 4581 sosng 4582 optocl 4585 relcnvexb 5048 funimass1 5170 dmfex 5282 f1ocnvb 5349 eqfnfv2 5487 elpreima 5507 dff13 5637 f1ocnvfv 5648 f1ocnvfvb 5649 fliftfun 5665 eusvobj2 5728 mpoxopn0yelv 6104 rntpos 6122 erexb 6422 findcard2 6751 findcard2s 6752 xpfi 6786 sbthlemi3 6815 enq0tr 7210 addnqprllem 7303 addnqprulem 7304 distrlem1prl 7358 distrlem1pru 7359 recexprlem1ssl 7409 recexprlem1ssu 7410 elrealeu 7605 addcan 7910 addcan2 7911 neg11 7981 negreb 7995 mulcanapd 8390 receuap 8398 cju 8687 nn1suc 8707 nnaddcl 8708 nndivtr 8730 znegclb 9055 zaddcllempos 9059 zmulcl 9075 zeo 9124 uz11 9316 uzp1 9327 eqreznegel 9374 xneg11 9585 xnegdi 9619 modqadd1 10102 modqmul1 10118 frec2uzltd 10144 bccmpl 10468 fz1eqb 10505 cj11 10645 rennim 10742 resqrexlemgt0 10760 efne0 11311 dvdsabseq 11472 uptx 12370 hmeocnvb 12414 tgioo 12642 bj-nnbidc 12889 bj-prexg 13036 strcollnft 13109 |
Copyright terms: Public domain | W3C validator |