![]() |
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 1204 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl5 32 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | 3imp 1195 |
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 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: syl3an2b 1286 syl3an2br 1289 syl3anl2 1298 nndi 6512 nnmass 6513 prarloclemarch2 7449 1idprl 7620 1idpru 7621 recexprlem1ssl 7663 recexprlem1ssu 7664 msqge0 8604 mulge0 8607 divsubdirap 8696 divdiv32ap 8708 peano2uz 9615 fzoshftral 10270 expdivap 10605 bcval5 10778 redivap 10918 imdivap 10925 absdiflt 11136 absdifle 11137 retanclap 11765 tannegap 11771 lcmgcdeq 12118 isprm3 12153 prmdvdsexpb 12184 dvdsprmpweqnn 12371 mulgaddcomlem 13102 mulginvcom 13104 cnpf2 14184 blres 14411 |
Copyright terms: Public domain | W3C validator |