![]() |
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 2917 rmob 3055 preqr1g 3764 issod 4315 sotritrieq 4321 nsuceq0g 4414 suctr 4417 nordeq 4539 suc11g 4552 iss 4948 poirr2 5016 xp11m 5062 tz6.12c 5540 fnbrfvb 5551 fvelimab 5567 foeqcnvco 5784 f1eqcocnv 5785 acexmidlemcase 5863 nna0r 6472 nnawordex 6523 ectocld 6594 ecoptocl 6615 mapsn 6683 eqeng 6759 fopwdom 6829 ordiso 7028 ltexnqq 7385 nsmallnqq 7389 nqprloc 7522 aptiprleml 7616 map2psrprg 7782 0re 7935 lttri3 8014 0cnALT 8124 reapti 8513 recnz 9322 zneo 9330 uzn0 9519 flqidz 10259 ceilqidz 10289 modqid2 10324 modqmuladdnn0 10341 frec2uzrand 10378 frecuzrdgtcl 10385 seq3id 10481 seq3z 10484 facdiv 10689 facwordi 10691 maxleb 11196 fsumf1o 11369 dvdsnegb 11786 odd2np1lem 11847 odd2np1 11848 ltoddhalfle 11868 halfleoddlt 11869 opoe 11870 omoe 11871 opeo 11872 omeo 11873 gcddiv 11990 gcdzeq 11993 dvdssqim 11995 lcmgcdeq 12053 coprmdvds2 12063 rpmul 12068 divgcdcoprmex 12072 cncongr2 12074 dvdsprm 12107 coprm 12114 prmdvdsexp 12118 prmdiv 12205 pythagtriplem19 12252 pc2dvds 12299 pcadd 12309 prmpwdvds 12323 exmidunben 12397 intopsn 12665 ismgmid 12675 isgrpid2 12790 isgrpinv 12803 dfgrp3mlem 12844 dvdsrcl2 13080 dvdsrtr 13082 dvdsrmul1 13083 baspartn 13181 bastop 13208 isopn3 13258 lgsdir 14069 lgsne0 14072 bj-peano4 14329 sbthomlem 14396 |
Copyright terms: Public domain | W3C validator |