Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl5ibrcom | Unicode version |
Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.) |
Ref | Expression |
---|---|
syl5ibr.1 | |
syl5ibr.2 |
Ref | Expression |
---|---|
syl5ibrcom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5ibr.1 | . . 3 | |
2 | syl5ibr.2 | . . 3 | |
3 | 1, 2 | syl5ibr 155 | . 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 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biimprcd 159 elsn2g 3528 preqr1g 3663 opth1 4128 euotd 4146 tz7.2 4246 reusv3 4351 alxfr 4352 reuhypd 4362 ordsucim 4386 suc11g 4442 nlimsucg 4451 xpsspw 4621 funcnvuni 5162 fvmptdv2 5478 fsn 5560 fconst2g 5603 funfvima 5617 foco2 5623 isores3 5684 eusvobj2 5728 ovmpodv2 5872 ovelrn 5887 f1opw2 5944 suppssfv 5946 suppssov1 5947 nnmordi 6380 nnmord 6381 qsss 6456 eroveu 6488 th3qlem1 6499 mapsncnv 6557 elixpsn 6597 ixpsnf1o 6598 en1bg 6662 mapxpen 6710 en1eqsnbi 6805 updjud 6935 addnidpig 7112 enq0tr 7210 prcdnql 7260 prcunqu 7261 genipv 7285 genpelvl 7288 genpelvu 7289 distrlem5prl 7362 distrlem5pru 7363 aptiprlemu 7416 mulid1 7731 ltne 7817 cnegex 7908 creur 8685 creui 8686 cju 8687 nnsub 8727 un0addcl 8978 un0mulcl 8979 zaddcl 9062 elz2 9090 qmulz 9383 qre 9385 qnegcl 9396 xrltne 9564 xlesubadd 9634 iccid 9676 fzsn 9814 fzsuc2 9827 fz1sbc 9844 elfzp12 9847 modqmuladd 10107 bcval5 10477 bcpasc 10480 hashprg 10522 hashfzo 10536 shftlem 10556 replim 10599 sqrtsq 10784 absle 10829 maxabslemval 10948 negfi 10967 xrmaxiflemval 10987 summodclem2 11119 summodc 11120 zsumdc 11121 fsum3 11124 fsummulc2 11185 fsum00 11199 isumsplit 11228 fzo0dvdseq 11482 divalgmod 11551 gcdabs1 11604 dvdsgcd 11627 dvdsmulgcd 11640 lcmgcdeq 11691 isprm2lem 11724 dvdsprime 11730 coprm 11749 prmdvdsexpr 11755 rpexp 11758 phibndlem 11819 dfphi2 11823 hashgcdlem 11830 istopon 12107 eltg3 12153 tgidm 12170 restbasg 12264 tgrest 12265 tgcn 12304 cnconst 12330 lmss 12342 txbas 12354 txbasval 12363 upxp 12368 blssps 12523 blss 12524 metrest 12602 blssioo 12641 elcncf1di 12662 bj-peano4 13080 |
Copyright terms: Public domain | W3C validator |