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 8681 creui 8682 cju 8683 nnsub 8723 un0addcl 8968 un0mulcl 8969 zaddcl 9052 elz2 9080 qmulz 9371 qre 9373 qnegcl 9384 xrltne 9551 xlesubadd 9621 iccid 9663 fzsn 9801 fzsuc2 9814 fz1sbc 9831 elfzp12 9834 modqmuladd 10094 bcval5 10464 bcpasc 10467 hashprg 10509 hashfzo 10523 shftlem 10543 replim 10586 sqrtsq 10771 absle 10816 maxabslemval 10935 negfi 10954 xrmaxiflemval 10974 summodclem2 11106 summodc 11107 zsumdc 11108 fsum3 11111 fsummulc2 11172 fsum00 11186 isumsplit 11215 fzo0dvdseq 11467 divalgmod 11536 gcdabs1 11589 dvdsgcd 11612 dvdsmulgcd 11625 lcmgcdeq 11676 isprm2lem 11709 dvdsprime 11715 coprm 11734 prmdvdsexpr 11740 rpexp 11743 phibndlem 11803 dfphi2 11807 hashgcdlem 11814 istopon 12091 eltg3 12137 tgidm 12154 restbasg 12248 tgrest 12249 tgcn 12288 cnconst 12314 lmss 12326 txbas 12338 txbasval 12347 upxp 12352 blssps 12507 blss 12508 metrest 12586 blssioo 12625 elcncf1di 12646 bj-peano4 13049 |
Copyright terms: Public domain | W3C validator |