![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl2anb | Unicode version |
Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.) |
Ref | Expression |
---|---|
syl2anb.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl2anb.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl2anb.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl2anb |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2anb.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | syl2anb.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | syl2anb.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylanb 268 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | sylan2b 271 |
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 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: sylancb 395 reupick3 3216 difprsnss 3493 trin2 4659 imadiflem 4921 fnun 4948 fco 4999 f1co 5044 foco 5059 f1oun 5089 f1oco 5092 eqfunfv 5213 ftpg 5290 issmo 5844 tfrlem5 5871 ener 6195 domtr 6201 unen 6229 xpdom2 6241 axpre-lttrn 6768 axpre-mulgt0 6771 zmulcl 8073 qaddcl 8346 qmulcl 8348 rpaddcl 8381 rpmulcl 8382 rpdivcl 8383 xrltnsym 8484 xrlttri3 8488 ge0addcl 8620 ge0mulcl 8621 expclzaplem 8933 expge0 8945 expge1 8946 |
Copyright terms: Public domain | W3C validator |