Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylibd | GIF version |
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
sylibd.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
sylibd.2 | ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
sylibd | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylibd.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | sylibd.2 | . . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) | |
3 | 2 | biimpd 142 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
4 | 1, 3 | syld 44 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 3imtr3d 200 dvelimdf 1933 ceqsalt 2625 sbceqal 2869 csbiebt 2942 rspcsbela 2961 preqr1g 3558 repizf2 3936 copsexg 3999 onun2 4234 suc11g 4300 elrnrexdm 5327 isoselem 5479 riotass2 5514 nnm00 6125 ecopovtrn 6226 ecopovtrng 6229 infglbti 6438 enq0tr 6624 addnqprl 6719 addnqpru 6720 mulnqprl 6758 mulnqpru 6759 recexprlemss1l 6825 recexprlemss1u 6826 cauappcvgprlemdisj 6841 mulextsr1lem 6956 pitonn 7016 rereceu 7055 cnegexlem1 7283 ltadd2 7523 mulext 7714 mulgt1 7941 lt2halves 8266 addltmul 8267 nzadd 8403 zextlt 8439 recnz 8440 zeo 8452 peano5uzti 8455 irradd 8731 irrmul 8732 xltneg 8903 icc0r 8949 fznuz 9119 uznfz 9120 facndiv 9666 rennim 9888 abs00ap 9948 absle 9975 cau3lem 10000 caubnd2 10003 climshft 10143 subcn2 10150 mulcn2 10151 serif0 10189 moddvds 10204 dvdsssfz1 10252 nn0seqcvgd 10423 algcvgblem 10431 eucalglt 10439 lcmgcdlem 10459 rpmul 10480 divgcdcoprm0 10483 isprm6 10526 rpexp 10532 bj-peano4 10750 |
Copyright terms: Public domain | W3C validator |