![]() |
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 309 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | syl21anc.4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: issod 4319 brcogw 4796 funprg 5266 funtpg 5267 fnunsn 5323 ftpg 5700 fsnunf 5716 isotr 5816 off 6094 caofrss 6106 tfr1onlembxssdm 6343 tfrcllembxssdm 6356 pmresg 6675 ac6sfi 6897 tridc 6898 fidcenumlemrks 6951 sbthlemi8 6962 casefun 7083 caseinj 7087 djufun 7102 djuinj 7104 mulclpi 7326 archnqq 7415 addlocprlemlt 7529 addlocprlemeq 7531 addlocprlemgt 7532 mullocprlem 7568 apreim 8559 subrecap 8795 ltrec1 8844 divge0d 9736 fseq1p1m1 10093 q2submod 10384 seq3caopr2 10481 seq3distr 10512 facavg 10725 shftfibg 10828 sqrtdiv 11050 sqrtdivd 11176 mulcn2 11319 demoivreALT 11780 dvdslegcd 11964 gcdnncl 11967 qredeu 12096 rpdvds 12098 rpexp 12152 oddpwdclemodd 12171 divnumden 12195 divdenle 12196 phimullem 12224 phisum 12239 pythagtriplem4 12267 pythagtriplem8 12271 pythagtriplem9 12272 pcgcd1 12326 fldivp1 12345 pockthlem 12353 setsfun 12496 setsfun0 12497 strleund 12561 ercpbl 12749 mndpropd 12840 grpidssd 12945 grpinvssd 12946 issubg2m 13047 isnsg3 13065 eqgid 13083 comet 13969 fsumcncntop 14026 mulcncf 14061 2sqlem8a 14439 2sqlem8 14440 trilpo 14761 neapmkv 14785 |
Copyright terms: Public domain | W3C validator |