![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6bi | GIF 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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 19.33bdc 1590 ax11i 1673 equveli 1713 eupickbi 2055 rgen2a 2458 reu6 2840 sseq0 3368 disjel 3381 preq12b 3661 prel12 3662 prneimg 3665 elinti 3744 exmidundif 4087 opthreg 4429 elreldm 4723 issref 4877 relcnvtr 5014 relresfld 5024 funopg 5113 funimass2 5157 f0dom0 5272 fvimacnv 5487 elunirn 5619 oprabid 5755 op1steq 6029 f1o2ndf1 6077 reldmtpos 6102 rntpos 6106 nntri3or 6341 nnaordex 6375 nnawordex 6376 findcard2 6734 findcard2s 6735 mkvprop 6979 lt2addnq 7154 lt2mulnq 7155 genpelvl 7262 genpelvu 7263 distrlem5prl 7336 distrlem5pru 7337 caucvgprlemnkj 7416 rereceu 7618 ltxrlt 7748 0mnnnnn0 8907 elnnnn0b 8919 nn0le2is012 9031 btwnz 9068 uz11 9244 nn01to3 9305 zq 9314 xrltso 9469 xltnegi 9505 xnn0lenn0nn0 9535 xnn0xadd0 9537 iccleub 9601 fzdcel 9707 uznfz 9770 2ffzeq 9805 elfzonlteqm1 9874 flqeqceilz 9978 modqadd1 10021 modqmul1 10037 frecuzrdgtcl 10072 frecuzrdgfunlem 10079 fzfig 10090 m1expeven 10227 caucvgrelemcau 10638 rexico 10879 fisumss 11047 fsum2dlemstep 11089 0dvds 11355 alzdvds 11394 opoe 11434 omoe 11435 opeo 11436 omeo 11437 m1exp1 11440 nn0enne 11441 nn0o1gt2 11444 gcdneg 11512 dfgcd2 11542 algcvgblem 11570 algcvga 11572 eucalglt 11578 coprmdvds 11613 divgcdcoprmex 11623 cncongr1 11624 prm2orodd 11647 tg2 12066 tgcl 12070 neii1 12153 neii2 12155 txlm 12284 tgioo 12526 addcncntoplem 12531 bj-elssuniab 12681 bj-nn0sucALT 12859 triap 12905 |
Copyright terms: Public domain | W3C validator |