![]() |
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: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 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 3481 preqr1g 3616 opth1 4072 euotd 4090 tz7.2 4190 reusv3 4295 alxfr 4296 reuhypd 4306 ordsucim 4330 suc11g 4386 nlimsucg 4395 xpsspw 4563 funcnvuni 5096 fvmptdv2 5405 fsn 5483 fconst2g 5526 funfvima 5540 foco2 5547 isores3 5608 eusvobj2 5652 ovmpt2dv2 5792 ovelrn 5807 f1opw2 5864 suppssfv 5866 suppssov1 5867 nnmordi 6289 nnmord 6290 qsss 6365 eroveu 6397 th3qlem1 6408 mapsncnv 6466 elixpsn 6506 ixpsnf1o 6507 en1bg 6571 mapxpen 6618 en1eqsnbi 6712 updjud 6827 addnidpig 6956 enq0tr 7054 prcdnql 7104 prcunqu 7105 genipv 7129 genpelvl 7132 genpelvu 7133 distrlem5prl 7206 distrlem5pru 7207 aptiprlemu 7260 mulid1 7546 ltne 7631 cnegex 7721 creur 8480 creui 8481 cju 8482 nnsub 8522 un0addcl 8767 un0mulcl 8768 zaddcl 8851 elz2 8879 qmulz 9169 qre 9171 qnegcl 9182 xrltne 9339 iccid 9404 fzsn 9541 fzsuc2 9554 fz1sbc 9571 elfzp12 9574 modqmuladd 9834 iseqid3 9998 ibcval5 10232 bcpasc 10235 hashprg 10277 hashfzo 10291 shftlem 10311 replim 10354 sqrtsq 10538 absle 10583 maxabslemval 10702 negfi 10720 isummolem2 10833 isummo 10834 zisum 10835 fisum 10839 fsummulc2 10903 fsum00 10917 isumsplit 10946 fzo0dvdseq 11197 divalgmod 11266 gcdabs1 11319 dvdsgcd 11340 dvdsmulgcd 11353 lcmgcdeq 11404 isprm2lem 11437 dvdsprime 11443 coprm 11462 prmdvdsexpr 11468 rpexp 11471 phibndlem 11531 dfphi2 11535 hashgcdlem 11542 istopon 11773 eltg3 11818 tgidm 11835 elcncf1di 11908 bj-peano4 12123 |
Copyright terms: Public domain | W3C validator |