Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl3an2 | Unicode version |
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
Ref | Expression |
---|---|
syl3an2.1 | |
syl3an2.2 |
Ref | Expression |
---|---|
syl3an2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3an2.1 | . . 3 | |
2 | syl3an2.2 | . . . 4 | |
3 | 2 | 3exp 1137 | . . 3 |
4 | 1, 3 | syl5 32 | . 2 |
5 | 4 | 3imp 1132 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 919 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 921 |
This theorem is referenced by: syl3an2b 1206 syl3an2br 1209 syl3anl2 1218 nndi 6088 nnmass 6089 prarloclemarch2 6609 1idprl 6780 1idpru 6781 recexprlem1ssl 6823 recexprlem1ssu 6824 msqge0 7716 mulge0 7719 divsubdirap 7796 divdiv32ap 7808 peano2uz 8671 fzoshftral 9247 expdivap 9527 ibcval5 9690 redivap 9761 imdivap 9768 absdiflt 9978 absdifle 9979 lcmgcdeq 10465 isprm3 10500 prmdvdsexpb 10528 |
Copyright terms: Public domain | W3C validator |