![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl2anb | Structured version Visualization version 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 475 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | sylan2b 478 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 189 df-an 373 |
This theorem is referenced by: sylancb 670 reupick3 3727 difprsnss 4106 pwssun 4739 trin2 5222 sspred 5387 fnun 5680 fco 5737 f1co 5786 foco 5801 f1oun 5831 f1oco 5834 eqfnfv 5974 eqfunfv 5979 sorpsscmpl 6579 ordsucsssuc 6647 ordsucun 6649 soxp 6906 ressuppssdif 6933 wfrlem4 7036 issmo 7064 tfrlem5 7095 ener 7613 domtr 7619 unen 7649 xpdom2 7664 mapen 7733 unxpdomlem3 7775 fiin 7933 suc11reg 8121 xpnum 8382 pm54.43 8431 r0weon 8440 fseqen 8455 kmlem9 8585 axpre-lttrn 9587 axpre-mulgt0 9589 wloglei 10143 mulnzcnopr 10255 zaddcl 10974 zmulcl 10982 qaddcl 11277 qmulcl 11279 rpaddcl 11320 rpmulcl 11321 rpdivcl 11322 xrltnsym 11433 xrlttri 11435 xmullem 11547 xmulcom 11549 xmulneg1 11552 xmulf 11555 ge0addcl 11741 ge0mulcl 11742 ge0xaddcl 11743 ge0xmulcl 11744 serge0 12264 expclzlem 12293 expge0 12305 expge1 12306 hashfacen 12614 wwlktovf1 13025 qredeu 14657 nn0gcdsq 14694 mul4sq 14891 fpwipodrs 16403 gimco 16925 gictr 16932 symgextf1 17055 efgrelexlemb 17393 xrs1mnd 18999 lmimco 19395 lmictra 19396 iscn2 20247 iscnp2 20248 paste 20303 txuni 20600 txcn 20634 txcmpb 20652 tx2ndc 20659 hmphtr 20791 snfil 20872 supfil 20903 filssufilg 20919 tsmsxp 21162 dscmet 21580 rlimcnp 23884 efnnfsumcl 24022 efchtdvds 24079 lgsne0 24254 mul2sq 24286 colinearalglem2 24930 nb3graprlem2 25173 wlkntrllem3 25284 wlknwwlknsur 25433 wlkiswwlksur 25440 wwlkextinj 25451 frgra3v 25723 ablosn 26068 ablomul 26076 hsn0elch 26894 shscli 26963 hsupss 26987 5oalem6 27305 mdsldmd1i 27977 superpos 28000 bnj110 29662 msubco 30162 ghomsn 30299 poseq 30484 frrlem4 30510 sltsolem1 30550 fnsingle 30679 funimage 30688 funpartfun 30703 bj-snsetex 31550 riscer 32220 divrngidl 32254 mzpincl 35570 kelac2lem 35916 rp-fakenanass 36153 cllem0 36164 unhe1 36375 tz6.12-1-afv 38670 nb3grprlem2 39438 cplgr3v 39485 2zrngamgm 39926 2zrngmmgm 39933 |
Copyright terms: Public domain | W3C validator |