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 2079 rgen2a 2484 reu6 2868 sseq0 3399 disjel 3412 preq12b 3692 prel12 3693 prneimg 3696 elinti 3775 exmidundif 4124 opthreg 4466 elreldm 4760 issref 4916 relcnvtr 5053 relresfld 5063 funopg 5152 funimass2 5196 f0dom0 5311 fvimacnv 5528 elunirn 5660 oprabid 5796 op1steq 6070 f1o2ndf1 6118 reldmtpos 6143 rntpos 6147 nntri3or 6382 nnaordex 6416 nnawordex 6417 findcard2 6776 findcard2s 6777 mkvprop 7025 lt2addnq 7205 lt2mulnq 7206 genpelvl 7313 genpelvu 7314 distrlem5prl 7387 distrlem5pru 7388 caucvgprlemnkj 7467 map2psrprg 7606 rereceu 7690 ltxrlt 7823 0mnnnnn0 9002 elnnnn0b 9014 nn0le2is012 9126 btwnz 9163 uz11 9341 nn01to3 9402 zq 9411 xrltso 9575 xltnegi 9611 xnn0lenn0nn0 9641 xnn0xadd0 9643 iccleub 9707 fzdcel 9813 uznfz 9876 2ffzeq 9911 elfzonlteqm1 9980 flqeqceilz 10084 modqadd1 10127 modqmul1 10143 frecuzrdgtcl 10178 frecuzrdgfunlem 10185 fzfig 10196 m1expeven 10333 caucvgrelemcau 10745 rexico 10986 fisumss 11154 fsum2dlemstep 11196 ntrivcvgap 11310 0dvds 11502 alzdvds 11541 opoe 11581 omoe 11582 opeo 11583 omeo 11584 m1exp1 11587 nn0enne 11588 nn0o1gt2 11591 gcdneg 11659 dfgcd2 11691 algcvgblem 11719 algcvga 11721 eucalglt 11727 coprmdvds 11762 divgcdcoprmex 11772 cncongr1 11773 prm2orodd 11796 tg2 12218 tgcl 12222 neii1 12305 neii2 12307 txlm 12437 reopnap 12696 tgioo 12704 addcncntoplem 12709 bj-elssuniab 12987 bj-nn0sucALT 13165 triap 13213 |
Copyright terms: Public domain | W3C validator |