Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6bi | Unicode version |
Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.) |
Ref | Expression |
---|---|
syl6bi.1 | |
syl6bi.2 |
Ref | Expression |
---|---|
syl6bi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6bi.1 | . . 3 | |
2 | 1 | biimpd 143 | . 2 |
3 | syl6bi.2 | . 2 | |
4 | 2, 3 | syl6 33 | 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: 19.33bdc 1609 ax11i 1692 equveli 1732 eupickbi 2081 rgen2a 2486 reu6 2873 sseq0 3404 disjel 3417 preq12b 3697 prel12 3698 prneimg 3701 elinti 3780 exmidundif 4129 opthreg 4471 elreldm 4765 issref 4921 relcnvtr 5058 relresfld 5068 funopg 5157 funimass2 5201 f0dom0 5316 fvimacnv 5535 elunirn 5667 oprabid 5803 op1steq 6077 f1o2ndf1 6125 reldmtpos 6150 rntpos 6154 nntri3or 6389 nnaordex 6423 nnawordex 6424 findcard2 6783 findcard2s 6784 mkvprop 7032 lt2addnq 7212 lt2mulnq 7213 genpelvl 7320 genpelvu 7321 distrlem5prl 7394 distrlem5pru 7395 caucvgprlemnkj 7474 map2psrprg 7613 rereceu 7697 ltxrlt 7830 0mnnnnn0 9009 elnnnn0b 9021 nn0le2is012 9133 btwnz 9170 uz11 9348 nn01to3 9409 zq 9418 xrltso 9582 xltnegi 9618 xnn0lenn0nn0 9648 xnn0xadd0 9650 iccleub 9714 fzdcel 9820 uznfz 9883 2ffzeq 9918 elfzonlteqm1 9987 flqeqceilz 10091 modqadd1 10134 modqmul1 10150 frecuzrdgtcl 10185 frecuzrdgfunlem 10192 fzfig 10203 m1expeven 10340 caucvgrelemcau 10752 rexico 10993 fisumss 11161 fsum2dlemstep 11203 ntrivcvgap 11317 0dvds 11513 alzdvds 11552 opoe 11592 omoe 11593 opeo 11594 omeo 11595 m1exp1 11598 nn0enne 11599 nn0o1gt2 11602 gcdneg 11670 dfgcd2 11702 algcvgblem 11730 algcvga 11732 eucalglt 11738 coprmdvds 11773 divgcdcoprmex 11783 cncongr1 11784 prm2orodd 11807 tg2 12229 tgcl 12233 neii1 12316 neii2 12318 txlm 12448 reopnap 12707 tgioo 12715 addcncntoplem 12720 bj-elssuniab 12998 bj-nn0sucALT 13176 triap 13224 |
Copyright terms: Public domain | W3C validator |