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 4194 posng 4681 sosng 4682 optocl 4685 relcnvexb 5148 funimass1 5273 dmfex 5385 f1ocnvb 5454 eqfnfv2 5592 elpreima 5612 dff13 5744 f1ocnvfv 5755 f1ocnvfvb 5756 fliftfun 5772 eusvobj2 5836 mpoxopn0yelv 6215 rntpos 6233 erexb 6534 findcard2 6863 findcard2s 6864 xpfi 6903 sbthlemi3 6932 enq0tr 7383 addnqprllem 7476 addnqprulem 7477 distrlem1prl 7531 distrlem1pru 7532 recexprlem1ssl 7582 recexprlem1ssu 7583 elrealeu 7778 addcan 8086 addcan2 8087 neg11 8157 negreb 8171 mulcanapd 8566 receuap 8574 cju 8864 nn1suc 8884 nnaddcl 8885 nndivtr 8907 znegclb 9232 zaddcllempos 9236 zmulcl 9252 zeo 9304 uz11 9496 uzp1 9507 eqreznegel 9560 xneg11 9778 xnegdi 9812 modqadd1 10304 modqmul1 10320 frec2uzltd 10346 bccmpl 10675 fz1eqb 10712 cj11 10856 rennim 10953 resqrexlemgt0 10971 efne0 11628 dvdsabseq 11794 pcfac 12289 grpinveu 12728 uptx 13027 hmeocnvb 13071 tgioo 13299 bj-nnbidc 13751 bj-prexg 13906 strcollnft 13979 |
Copyright terms: Public domain | W3C validator |