![]() |
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 154 |
. 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 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: biimprcd 158 elsn2g 3477 preqr1g 3610 opth1 4063 euotd 4081 tz7.2 4181 reusv3 4282 alxfr 4283 reuhypd 4293 ordsucim 4317 suc11g 4373 nlimsucg 4382 xpsspw 4550 funcnvuni 5083 fvmptdv2 5392 fsn 5469 fconst2g 5512 funfvima 5526 foco2 5533 isores3 5594 eusvobj2 5638 ovmpt2dv2 5778 ovelrn 5793 f1opw2 5850 suppssfv 5852 suppssov1 5853 nnmordi 6273 nnmord 6274 qsss 6349 eroveu 6381 th3qlem1 6392 mapsncnv 6450 en1bg 6515 mapxpen 6562 en1eqsnbi 6656 updjud 6771 addnidpig 6893 enq0tr 6991 prcdnql 7041 prcunqu 7042 genipv 7066 genpelvl 7069 genpelvu 7070 distrlem5prl 7143 distrlem5pru 7144 aptiprlemu 7197 mulid1 7483 ltne 7568 cnegex 7658 creur 8417 creui 8418 cju 8419 nnsub 8459 un0addcl 8704 un0mulcl 8705 zaddcl 8788 elz2 8816 qmulz 9106 qre 9108 qnegcl 9119 xrltne 9276 iccid 9341 fzsn 9477 fzsuc2 9489 fz1sbc 9506 elfzp12 9509 modqmuladd 9769 iseqid3 9933 ibcval5 10167 bcpasc 10170 hashprg 10212 hashfzo 10226 shftlem 10246 replim 10289 sqrtsq 10473 absle 10518 maxabslemval 10637 negfi 10655 isummolem2 10768 isummo 10769 zisum 10770 fisum 10774 fsummulc2 10838 fsum00 10852 isumsplit 10881 fzo0dvdseq 11132 divalgmod 11201 gcdabs1 11254 dvdsgcd 11275 dvdsmulgcd 11288 lcmgcdeq 11339 isprm2lem 11372 dvdsprime 11378 coprm 11397 prmdvdsexpr 11403 rpexp 11406 phibndlem 11466 dfphi2 11470 hashgcdlem 11477 istopon 11565 elcncf1di 11590 bj-peano4 11805 |
Copyright terms: Public domain | W3C validator |