![]() |
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 1162 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | syl13anc.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 1, 5, 6 | syl2anc 409 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: syl23anc 1224 syl33anc 1232 caovassd 5938 caovcand 5941 caovordid 5945 caovordd 5947 caovdid 5954 caovdird 5957 swoer 6465 swoord1 6466 swoord2 6467 fimax2gtrilemstep 6802 iunfidisj 6842 ssfii 6870 suplub2ti 6896 prarloclem3 7329 fzosubel3 10004 seq3split 10283 seq3caopr 10287 zsumdc 11185 fsumiun 11278 divalglemex 11655 strle1g 12088 psmetsym 12537 psmettri 12538 psmetge0 12539 psmetres2 12541 xmetge0 12573 xmetsym 12576 xmettri 12580 metrtri 12585 xmetres2 12587 bldisj 12609 xblss2ps 12612 xblss2 12613 xmeter 12644 xmetxp 12715 |
Copyright terms: Public domain | W3C validator |