![]() |
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 1142 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl5 32 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | 3imp 1137 |
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 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 926 |
This theorem is referenced by: syl3an2b 1211 syl3an2br 1214 syl3anl2 1223 nndi 6239 nnmass 6240 prarloclemarch2 6968 1idprl 7139 1idpru 7140 recexprlem1ssl 7182 recexprlem1ssu 7183 msqge0 8083 mulge0 8086 divsubdirap 8165 divdiv32ap 8177 peano2uz 9061 fzoshftral 9637 expdivap 9994 ibcval5 10159 redivap 10296 imdivap 10303 absdiflt 10513 absdifle 10514 retanclap 11000 tannegap 11006 lcmgcdeq 11330 isprm3 11365 prmdvdsexpb 11393 |
Copyright terms: Public domain | W3C validator |