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 |
---|---|
syl5ib.1 | |
syl5ib.2 |
Ref | Expression |
---|---|
syl5ibcom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5ib.1 | . . 3 | |
2 | syl5ib.2 | . . 3 | |
3 | 1, 2 | syl5ib 153 | . 2 |
4 | 3 | com12 30 | 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: biimpcd 158 mob2 2837 rmob 2973 preqr1g 3663 issod 4211 sotritrieq 4217 nsuceq0g 4310 suctr 4313 nordeq 4429 suc11g 4442 iss 4835 poirr2 4901 xp11m 4947 tz6.12c 5419 fnbrfvb 5430 fvelimab 5445 foeqcnvco 5659 f1eqcocnv 5660 acexmidlemcase 5737 nna0r 6342 nnawordex 6392 ectocld 6463 ecoptocl 6484 mapsn 6552 eqeng 6628 fopwdom 6698 ordiso 6889 ltexnqq 7184 nsmallnqq 7188 nqprloc 7321 aptiprleml 7415 map2psrprg 7581 0re 7734 lttri3 7812 0cnALT 7920 reapti 8309 recnz 9112 zneo 9120 uzn0 9309 flqidz 10027 ceilqidz 10057 modqid2 10092 modqmuladdnn0 10109 frec2uzrand 10146 frecuzrdgtcl 10153 seq3id 10249 seq3z 10252 facdiv 10452 facwordi 10454 maxleb 10956 fsumf1o 11127 dvdsnegb 11437 odd2np1lem 11496 odd2np1 11497 ltoddhalfle 11517 halfleoddlt 11518 opoe 11519 omoe 11520 opeo 11521 omeo 11522 gcddiv 11634 gcdzeq 11637 dvdssqim 11639 lcmgcdeq 11691 coprmdvds2 11701 rpmul 11706 divgcdcoprmex 11710 cncongr2 11712 dvdsprm 11744 coprm 11749 prmdvdsexp 11753 exmidunben 11866 baspartn 12144 bastop 12171 isopn3 12221 bj-peano4 13080 sbthomlem 13147 |
Copyright terms: Public domain | W3C validator |