![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylancr | GIF version |
Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Ref | Expression |
---|---|
sylancr.1 | ⊢ ψ |
sylancr.2 | ⊢ (φ → χ) |
sylancr.3 | ⊢ ((ψ ∧ χ) → θ) |
Ref | Expression |
---|---|
sylancr | ⊢ (φ → θ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylancr.1 | . . 3 ⊢ ψ | |
2 | 1 | a1i 9 | . 2 ⊢ (φ → ψ) |
3 | sylancr.2 | . 2 ⊢ (φ → χ) | |
4 | sylancr.3 | . 2 ⊢ ((ψ ∧ χ) → θ) | |
5 | 2, 3, 4 | syl2anc 391 | 1 ⊢ (φ → θ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 |
This theorem is referenced by: mpteq2da 3837 unipw 3944 opeluu 4148 uniexb 4171 unon 4202 opeliunxp 4338 xpexg 4395 resiexg 4596 imaexg 4623 exse2 4642 soirri 4662 djudisj 4693 elxp5 4752 cnvexg 4798 cnviinm 4802 coexg 4805 funssres 4885 f1oabexg 5081 sefvex 5139 ssimaex 5177 mptfvex 5199 f1ompt 5263 fmptcof 5274 resfunexg 5325 mptexg 5329 funfvima3 5335 ovid 5559 ov 5562 ofres 5667 cofunexg 5680 opabex3d 5690 opabex3 5691 oprabexd 5696 1stcof 5732 2ndcof 5733 mpt2exxg 5775 cnvf1o 5788 f2ndf 5789 tposexg 5814 tfrlemisucaccv 5880 tfrlemibxssdm 5882 tfrlemibfn 5883 tfrlemi14d 5888 rdgtfr 5901 rdgruledefgg 5902 frecabex 5923 omcl 5980 erth 6086 th3qlem1 6144 fundmen 6222 snfig 6227 unen 6229 xpdom2 6241 ltnnnq 6406 nnnq0lem1 6429 addnqprlemfl 6540 addnqprlemfu 6541 prsrlem1 6670 gt0srpr 6676 mulcnsr 6732 mulcnsrec 6740 axmulass 6757 axdistr 6758 mulid1 6822 axmulgt0 6888 cnegexlem2 6984 cnegex 6986 gt0ne0d 7299 recexre 7362 msqge0 7400 mulge0 7403 recgt0 7597 recreclt 7647 cju 7694 nnge1 7718 nnnlt1 7721 nn0nlt0 7984 elz2 8088 nnm1ge0 8102 recnz 8109 zneo 8115 uz3m2nn 8291 eluz2b2 8316 nn01to3 8328 mnflt 8474 lincmb01cmp 8641 iccf1o 8642 fz1n 8678 fseq1p1m1 8726 fznn0 8744 fzctr 8761 4fvwrd4 8767 elfzonlteqm1 8836 frec2uzf1od 8873 frecuzrdgrom 8877 frecfzennn 8884 frecfzen2 8885 fzfig 8887 expgt1 8947 expubnd 8965 binom2sub 9017 binom3 9019 zesq 9020 bernneq 9022 bernneq2 9023 expnbnd 9025 expnlbnd2 9027 crre 9085 crim 9086 remim 9088 mulreap 9092 cjreb 9094 recj 9095 reneg 9096 readd 9097 remullem 9099 imcj 9103 imneg 9104 imadd 9105 cjadd 9112 cjneg 9118 imval2 9122 cjreim 9131 cnrecnv 9138 absval 9210 rennim 9211 |
Copyright terms: Public domain | W3C validator |