![]() |
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 284 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | sylan2b 287 |
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 |
This theorem is referenced by: sylancb 418 stdcndc 845 reupick3 3420 difprsnss 3730 trin2 5020 imadiflem 5295 fnun 5322 fco 5381 f1co 5433 foco 5448 f1oun 5481 f1oco 5484 eqfunfv 5618 ftpg 5700 issmo 6288 tfrlem5 6314 ener 6778 domtr 6784 unen 6815 xpdom2 6830 mapen 6845 pm54.43 7188 axpre-lttrn 7882 axpre-mulgt0 7885 zmulcl 9304 qaddcl 9633 qmulcl 9635 rpaddcl 9675 rpmulcl 9676 rpdivcl 9677 xrltnsym 9791 xrlttri3 9795 ge0addcl 9979 ge0mulcl 9980 ge0xaddcl 9981 expclzaplem 10541 expge0 10553 expge1 10554 hashfacen 10811 qredeu 12091 nn0gcdsq 12194 mul4sq 12386 cnovex 13627 iscn2 13631 txuni 13694 txcn 13706 lgsne0 14370 mul2sq 14383 |
Copyright terms: Public domain | W3C validator |