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 1161 | . 2 |
5 | sylXanc.4 | . 2 | |
6 | syl31anc.5 | . 2 | |
7 | 4, 5, 6 | syl2anc 408 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: syl32anc 1224 stoic4b 1409 enq0tr 7235 ltmul12a 8611 lt2msq1 8636 ledivp1 8654 lemul1ad 8690 lemul2ad 8691 lediv2ad 9499 xaddge0 9654 difelfznle 9905 expubnd 10343 expcanlem 10455 expcand 10457 xrmaxaddlem 11022 mertenslemi1 11297 eftlub 11385 dvdsadd 11525 divalgmod 11613 gcdzeq 11699 rplpwr 11704 sqgcd 11706 bezoutr 11709 rpmulgcd2 11765 rpdvds 11769 divgcdodd 11810 oddpwdclemxy 11836 divnumden 11863 crth 11889 phimullem 11890 xblss2ps 12562 xblss2 12563 metcnpi3 12675 limcimolemlt 12791 limccnp2cntop 12804 dvmulxxbr 12824 dvcoapbr 12829 |
Copyright terms: Public domain | W3C validator |