![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imbitrid | Unicode version |
Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.) |
Ref | Expression |
---|---|
imbitrid.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
imbitrid.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
imbitrid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbitrid.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | imbitrid.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | biimpd 144 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl5 32 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: syl5ibcom 155 imbitrrid 156 sbft 1848 gencl 2769 spsbc 2974 prexg 4211 posng 4698 sosng 4699 optocl 4702 relcnvexb 5168 funimass1 5293 dmfex 5405 f1ocnvb 5475 eqfnfv2 5614 elpreima 5635 dff13 5768 f1ocnvfv 5779 f1ocnvfvb 5780 fliftfun 5796 eusvobj2 5860 mpoxopn0yelv 6239 rntpos 6257 erexb 6559 findcard2 6888 findcard2s 6889 xpfi 6928 sbthlemi3 6957 enq0tr 7432 addnqprllem 7525 addnqprulem 7526 distrlem1prl 7580 distrlem1pru 7581 recexprlem1ssl 7631 recexprlem1ssu 7632 elrealeu 7827 addcan 8135 addcan2 8136 neg11 8206 negreb 8220 mulcanapd 8616 receuap 8624 cju 8916 nn1suc 8936 nnaddcl 8937 nndivtr 8959 znegclb 9284 zaddcllempos 9288 zmulcl 9304 zeo 9356 uz11 9548 uzp1 9559 eqreznegel 9612 xneg11 9832 xnegdi 9866 modqadd1 10358 modqmul1 10374 frec2uzltd 10400 bccmpl 10729 fz1eqb 10765 cj11 10909 rennim 11006 resqrexlemgt0 11024 efne0 11681 dvdsabseq 11847 pcfac 12342 grpinveu 12865 mulgass 12973 dvreq1 13264 uptx 13667 hmeocnvb 13711 tgioo 13939 bj-nnbidc 14391 bj-prexg 14545 strcollnft 14618 |
Copyright terms: Public domain | W3C validator |