![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl121anc | Unicode version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.4 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl121anc.5 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl121anc |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylXanc.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | sylXanc.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | jca 306 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | sylXanc.4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
6 | syl121anc.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 1, 4, 5, 6 | syl3anc 1249 |
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: syl122anc 1258 tfisi 4604 tfrcllemsucfn 6379 sbthlemi6 6992 sbthlemi8 6994 div32apd 8802 div13apd 8803 expdivapd 10702 modfsummodlemstep 11500 pcqmul 12338 pcid 12359 pcneg 12360 pc2dvds 12365 pcz 12367 pcaddlem 12374 pcadd 12375 pcmpt2 12379 pcbc 12386 qexpz 12387 expnprm 12388 ennnfonelemg 12457 ssblex 14408 |
Copyright terms: Public domain | W3C validator |