Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylcom | Unicode version |
Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.) |
Ref | Expression |
---|---|
sylcom.1 | |
sylcom.2 |
Ref | Expression |
---|---|
sylcom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylcom.1 | . 2 | |
2 | sylcom.2 | . . 3 | |
3 | 2 | a2i 11 | . 2 |
4 | 1, 3 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: syl5com 29 syl6 33 syli 37 mpbidi 150 stdcn 817 con4biddc 827 jaddc 834 con1biddc 846 necon4addc 2355 necon4bddc 2356 necon4ddc 2357 necon1addc 2361 necon1bddc 2362 dmcosseq 4780 iss 4835 funopg 5127 snon0 6792 metrest 12602 |
Copyright terms: Public domain | W3C validator |