![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syld3an3 | Unicode version |
Description: A syllogism inference. (Contributed by NM, 20-May-2007.) |
Ref | Expression |
---|---|
syld3an3.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syld3an3.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syld3an3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 997 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | simp2 998 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | syld3an3.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | syld3an3.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | syl3anc 1238 |
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 980 |
This theorem is referenced by: syld3an1 1284 syld3an2 1285 brelrng 4858 moriotass 5858 nnncan1 8192 lediv1 8825 modqval 10323 modqvalr 10324 modqcl 10325 flqpmodeq 10326 modq0 10328 modqge0 10331 modqlt 10332 modqdiffl 10334 modqdifz 10335 modqvalp1 10342 exp3val 10521 bcval4 10731 dvdsmultr1 11837 dvdssub2 11841 divalglemeuneg 11927 ndvdsadd 11935 grpsubf 12948 grpinvsub 12951 grpnpcan 12961 mulginvcom 13006 mulginvinv 13007 subgsubcl 13043 dvrcl 13302 unitdvcl 13303 basgen2 13517 opnneiss 13594 cnpf2 13643 sincosq1lem 14182 |
Copyright terms: Public domain | W3C validator |