![]() |
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 1163 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl5 32 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | 3imp 1158 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 947 |
This theorem is referenced by: syl3an2b 1236 syl3an2br 1239 syl3anl2 1248 nndi 6336 nnmass 6337 prarloclemarch2 7175 1idprl 7346 1idpru 7347 recexprlem1ssl 7389 recexprlem1ssu 7390 msqge0 8296 mulge0 8299 divsubdirap 8381 divdiv32ap 8393 peano2uz 9280 fzoshftral 9908 expdivap 10237 bcval5 10402 redivap 10539 imdivap 10546 absdiflt 10756 absdifle 10757 retanclap 11280 tannegap 11286 lcmgcdeq 11610 isprm3 11645 prmdvdsexpb 11673 cnpf2 12218 blres 12423 |
Copyright terms: Public domain | W3C validator |