![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl32anc | Unicode version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.4 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.5 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl32anc.6 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl32anc |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylXanc.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | sylXanc.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | sylXanc.4 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | sylXanc.5 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | jca 306 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | syl32anc.6 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 1, 2, 3, 6, 7 | syl31anc 1251 |
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 981 |
This theorem is referenced by: ioom 10275 modifeq2int 10400 modaddmodup 10401 seq3f1olemqsum 10514 seq3f1o 10518 exple1 10590 leexp2rd 10698 nn0ltexp2 10703 facubnd 10739 permnn 10765 dfabsmax 11240 expcnvre 11525 dvdsadd2b 11861 dvdsmulgcd 12040 sqgcd 12044 bezoutr 12047 cncongr2 12118 pw2dvds 12180 hashgcdlem 12252 modprm0 12268 modprmn0modprm0 12270 2idlcpblrng 13768 tgioo 14399 lgssq 14794 lgssq2 14795 |
Copyright terms: Public domain | W3C validator |