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 1191 | . . 3 |
4 | 1, 3 | syl5 32 | . 2 |
5 | 4 | 3imp 1182 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 967 |
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 969 |
This theorem is referenced by: syl3an2b 1264 syl3an2br 1267 syl3anl2 1276 nndi 6445 nnmass 6446 prarloclemarch2 7351 1idprl 7522 1idpru 7523 recexprlem1ssl 7565 recexprlem1ssu 7566 msqge0 8505 mulge0 8508 divsubdirap 8595 divdiv32ap 8607 peano2uz 9512 fzoshftral 10163 expdivap 10496 bcval5 10665 redivap 10802 imdivap 10809 absdiflt 11020 absdifle 11021 retanclap 11649 tannegap 11655 lcmgcdeq 11994 isprm3 12029 prmdvdsexpb 12060 dvdsprmpweqnn 12246 cnpf2 12754 blres 12981 |
Copyright terms: Public domain | W3C validator |