![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl13anc | Unicode version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.4 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl13anc.5 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl13anc |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylXanc.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | sylXanc.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | sylXanc.4 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3jca 1126 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | syl13anc.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 1, 5, 6 | syl2anc 404 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: syl23anc 1188 syl33anc 1196 caovassd 5842 caovcand 5845 caovordid 5849 caovordd 5851 caovdid 5858 caovdird 5861 swoer 6360 swoord1 6361 swoord2 6362 fimax2gtrilemstep 6696 iunfidisj 6735 suplub2ti 6776 prarloclem3 7153 fzosubel3 9756 seq3split 10045 seq3caopr 10049 zsumdc 10943 fsumiun 11036 divalglemex 11365 strle1g 11749 psmetsym 12131 psmettri 12132 psmetge0 12133 psmetres2 12135 xmetge0 12167 xmetsym 12170 xmettri 12174 metrtri 12179 xmetres2 12181 bldisj 12203 xblss2ps 12206 xblss2 12207 xmeter 12238 |
Copyright terms: Public domain | W3C validator |