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-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: syl5com 29 syl6 33 syli 37 mpbidi 149 con4biddc 787 jaddc 794 con1biddc 803 necon4addc 2315 necon4bddc 2316 necon4ddc 2317 necon1addc 2321 necon1bddc 2322 dmcosseq 4621 iss 4674 funopg 4954 snon0 6387 |
Copyright terms: Public domain | W3C validator |