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 8389 receuap 8397 cju 8683 nn1suc 8703 nnaddcl 8704 nndivtr 8726 znegclb 9045 zaddcllempos 9049 zmulcl 9065 zeo 9114 uz11 9304 uzp1 9315 eqreznegel 9362 xneg11 9572 xnegdi 9606 modqadd1 10089 modqmul1 10105 frec2uzltd 10131 bccmpl 10455 fz1eqb 10492 cj11 10632 rennim 10729 resqrexlemgt0 10747 efne0 11298 dvdsabseq 11457 uptx 12354 hmeocnvb 12398 tgioo 12626 bj-nnbidc 12858 bj-prexg 13005 strcollnft 13078 |
Copyright terms: Public domain | W3C validator |