| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > syl5ibcom | Unicode version | ||
| Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.) |
| Ref | Expression |
|---|---|
| imbitrid.1 |
|
| imbitrid.2 |
|
| Ref | Expression |
|---|---|
| syl5ibcom |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imbitrid.1 |
. . 3
| |
| 2 | imbitrid.2 |
. . 3
| |
| 3 | 1, 2 | imbitrid 154 |
. 2
|
| 4 | 3 | com12 30 |
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: biimpcd 159 mob2 2953 rmob 3091 preqr1g 3807 issod 4366 sotritrieq 4372 nsuceq0g 4465 suctr 4468 nordeq 4592 suc11g 4605 iss 5005 poirr2 5075 xp11m 5121 tz6.12c 5606 fnbrfvb 5619 fvelimab 5635 foeqcnvco 5859 f1eqcocnv 5860 acexmidlemcase 5939 nna0r 6564 nnawordex 6615 ectocld 6688 ecoptocl 6709 mapsn 6777 eqeng 6857 fopwdom 6933 ordiso 7138 ltexnqq 7521 nsmallnqq 7525 nqprloc 7658 aptiprleml 7752 map2psrprg 7918 0re 8072 lttri3 8152 0cnALT 8262 reapti 8652 recnz 9466 zneo 9474 uzn0 9664 flqidz 10429 ceilqidz 10461 modqid2 10496 modqmuladdnn0 10513 frec2uzrand 10550 frecuzrdgtcl 10557 seq3id 10670 seq3z 10673 facdiv 10883 facwordi 10885 wrdnval 11024 wrdl1s1 11084 maxleb 11527 fsumf1o 11701 dvdsnegb 12119 odd2np1lem 12183 odd2np1 12184 ltoddhalfle 12204 halfleoddlt 12205 opoe 12206 omoe 12207 opeo 12208 omeo 12209 gcddiv 12340 gcdzeq 12343 dvdssqim 12345 lcmgcdeq 12405 coprmdvds2 12415 rpmul 12420 divgcdcoprmex 12424 cncongr2 12426 dvdsprm 12459 coprm 12466 prmdvdsexp 12470 prmdiv 12557 pythagtriplem19 12605 pc2dvds 12653 pcadd 12663 prmpwdvds 12678 exmidunben 12797 intopsn 13199 ismgmid 13209 imasmnd2 13284 isgrpid2 13372 isgrpinv 13386 dfgrp3mlem 13430 imasgrp2 13446 imasrng 13718 imasring 13826 dvdsrcl2 13861 dvdsrtr 13863 dvdsrmul1 13864 lspsneq0 14188 dvdsrzring 14365 znunit 14421 baspartn 14522 bastop 14547 isopn3 14597 lgsdir 15512 lgsne0 15515 lgsquadlem3 15556 bj-peano4 15891 sbthomlem 15964 |
| Copyright terms: Public domain | W3C validator |