![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl31anc | Unicode version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.4 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl31anc.5 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl31anc |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylXanc.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | sylXanc.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3jca 1179 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | sylXanc.4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
6 | syl31anc.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 4, 5, 6 | syl2anc 411 |
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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: syl32anc 1257 stoic4b 1444 enq0tr 7464 ltmul12a 8848 lt2msq1 8873 ledivp1 8891 lemul1ad 8927 lemul2ad 8928 lediv2ad 9751 xaddge0 9910 difelfznle 10167 expubnd 10611 nn0leexp2 10725 expcanlem 10730 expcand 10732 xrmaxaddlem 11303 mertenslemi1 11578 eftlub 11733 dvdsadd 11878 divalgmod 11967 gcdzeq 12058 rplpwr 12063 sqgcd 12065 bezoutr 12068 rpmulgcd2 12130 rpdvds 12134 isprm5 12177 divgcdodd 12178 oddpwdclemxy 12204 divnumden 12231 crth 12259 phimullem 12260 coprimeprodsq2 12293 pythagtriplem19 12317 pclemub 12322 pcpre1 12327 pcidlem 12358 pockthlem 12391 prmunb 12397 kerf1ghm 13230 elrhmunit 13544 xblss2ps 14381 xblss2 14382 metcnpi3 14494 limcimolemlt 14610 limccnp2cntop 14623 dvmulxxbr 14643 dvcoapbr 14648 2lgsoddprmlem1 14931 2sqlem8a 14947 2sqlem8 14948 |
Copyright terms: Public domain | W3C validator |