![]() |
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: ![]() ![]() |
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 1610 ax11i 1693 equveli 1733 eupickbi 2082 rgen2a 2489 reu6 2877 sseq0 3409 disjel 3422 preq12b 3705 prel12 3706 prneimg 3709 elinti 3788 exmidundif 4137 opthreg 4479 elreldm 4773 issref 4929 relcnvtr 5066 relresfld 5076 funopg 5165 funimass2 5209 f0dom0 5324 fvimacnv 5543 elunirn 5675 oprabid 5811 op1steq 6085 f1o2ndf1 6133 reldmtpos 6158 rntpos 6162 nntri3or 6397 nnaordex 6431 nnawordex 6432 findcard2 6791 findcard2s 6792 mkvprop 7040 cc2lem 7098 lt2addnq 7236 lt2mulnq 7237 genpelvl 7344 genpelvu 7345 distrlem5prl 7418 distrlem5pru 7419 caucvgprlemnkj 7498 map2psrprg 7637 rereceu 7721 ltxrlt 7854 0mnnnnn0 9033 elnnnn0b 9045 nn0le2is012 9157 btwnz 9194 uz11 9372 nn01to3 9436 zq 9445 xrltso 9612 xltnegi 9648 xnn0lenn0nn0 9678 xnn0xadd0 9680 iccleub 9744 fzdcel 9851 uznfz 9914 2ffzeq 9949 elfzonlteqm1 10018 flqeqceilz 10122 modqadd1 10165 modqmul1 10181 frecuzrdgtcl 10216 frecuzrdgfunlem 10223 fzfig 10234 m1expeven 10371 caucvgrelemcau 10784 rexico 11025 fisumss 11193 fsum2dlemstep 11235 ntrivcvgap 11349 0dvds 11549 alzdvds 11588 opoe 11628 omoe 11629 opeo 11630 omeo 11631 m1exp1 11634 nn0enne 11635 nn0o1gt2 11638 gcdneg 11706 dfgcd2 11738 algcvgblem 11766 algcvga 11768 eucalglt 11774 coprmdvds 11809 divgcdcoprmex 11819 cncongr1 11820 prm2orodd 11843 tg2 12268 tgcl 12272 neii1 12355 neii2 12357 txlm 12487 reopnap 12746 tgioo 12754 addcncntoplem 12759 bj-elssuniab 13169 bj-nn0sucALT 13347 triap 13399 |
Copyright terms: Public domain | W3C validator |