Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl21anc | Unicode version |
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.) |
Ref | Expression |
---|---|
sylXanc.1 | |
sylXanc.2 | |
sylXanc.3 | |
syl21anc.4 |
Ref | Expression |
---|---|
syl21anc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . . 3 | |
2 | sylXanc.2 | . . 3 | |
3 | sylXanc.3 | . . 3 | |
4 | 1, 2, 3 | jca31 307 | . 2 |
5 | syl21anc.4 | . 2 | |
6 | 4, 5 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: issod 4291 brcogw 4767 funprg 5232 funtpg 5233 fnunsn 5289 ftpg 5663 fsnunf 5679 isotr 5778 off 6056 caofrss 6068 tfr1onlembxssdm 6302 tfrcllembxssdm 6315 pmresg 6633 ac6sfi 6855 tridc 6856 fidcenumlemrks 6909 sbthlemi8 6920 casefun 7041 caseinj 7045 djufun 7060 djuinj 7062 mulclpi 7260 archnqq 7349 addlocprlemlt 7463 addlocprlemeq 7465 addlocprlemgt 7466 mullocprlem 7502 apreim 8492 subrecap 8726 ltrec1 8774 divge0d 9664 fseq1p1m1 10019 q2submod 10310 seq3caopr2 10407 seq3distr 10438 facavg 10648 shftfibg 10748 sqrtdiv 10970 sqrtdivd 11096 mulcn2 11239 demoivreALT 11700 dvdslegcd 11882 gcdnncl 11885 qredeu 12008 rpdvds 12010 rpexp 12064 oddpwdclemodd 12083 divnumden 12107 divdenle 12108 phimullem 12136 phisum 12151 pythagtriplem4 12179 pythagtriplem8 12183 pythagtriplem9 12184 pcgcd1 12238 fldivp1 12257 pockthlem 12265 setsfun 12372 setsfun0 12373 strleund 12425 comet 13046 fsumcncntop 13103 mulcncf 13138 trilpo 13763 neapmkv 13787 |
Copyright terms: Public domain | W3C validator |