![]() |
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 144 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
4 | 1, 3 | syld 45 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3imtr3d 202 dvelimdf 2016 ceqsalt 2763 sbceqal 3018 csbiebt 3096 rspcsbela 3116 preqr1g 3766 repizf2 4162 copsexg 4244 onun2 4489 suc11g 4556 elrnrexdm 5655 isoselem 5820 riotass2 5856 oawordriexmid 6470 nnm00 6530 ecopovtrn 6631 ecopovtrng 6634 infglbti 7023 difinfsnlem 7097 enq0tr 7432 addnqprl 7527 addnqpru 7528 mulnqprl 7566 mulnqpru 7567 recexprlemss1l 7633 recexprlemss1u 7634 cauappcvgprlemdisj 7649 mulextsr1lem 7778 pitonn 7846 rereceu 7887 cnegexlem1 8131 ltadd2 8375 eqord2 8440 mulext 8570 mulgt1 8819 lt2halves 9153 addltmul 9154 nzadd 9304 ltsubnn0 9319 zextlt 9344 recnz 9345 zeo 9357 peano5uzti 9360 irradd 9645 irrmul 9646 xltneg 9835 xleadd1 9874 icc0r 9925 fznuz 10101 uznfz 10102 facndiv 10718 rennim 11010 abs00ap 11070 absle 11097 cau3lem 11122 caubnd2 11125 climshft 11311 subcn2 11318 mulcn2 11319 serf0 11359 cvgratnnlemnexp 11531 cvgratnnlemmn 11532 efieq1re 11778 moddvds 11805 dvdsssfz1 11857 nn0seqcvgd 12040 algcvgblem 12048 eucalglt 12056 lcmgcdlem 12076 rpmul 12097 divgcdcoprm0 12100 isprm6 12146 rpexp 12152 eulerthlema 12229 eulerthlemh 12230 prmdiv 12234 pcprendvds2 12290 pcz 12330 pcprmpw 12332 pcfac 12347 expnprm 12350 issubg4m 13051 tgss3 13514 cnpnei 13655 cnntr 13661 hmeoopn 13747 hmeocld 13748 mulcncflem 14026 sincosq3sgn 14185 sincosq4sgn 14186 lgsdir2lem4 14368 lgsne0 14375 2sqlem8a 14405 bj-peano4 14643 iswomni0 14735 |
Copyright terms: Public domain | W3C validator |