![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl6rbb | Structured version Visualization version Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6rbb.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl6rbb.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl6rbb |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6rbb.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | syl6rbb.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6bb 265 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | bicomd 205 |
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 |
This theorem is referenced by: syl6rbbr 268 bibif 348 pm5.61 718 oranabs 866 necon4bid 2668 resopab2 5152 xpco 5375 funconstss 5998 xpopth 6829 map1 7645 ac6sfi 7812 supgtoreq 7983 rankr1bg 8271 alephsdom 8514 brdom7disj 8956 fpwwe2lem13 9064 nn0sub 10917 elznn0 10949 nn01to3 11254 supxrbnd1 11604 supxrbnd2 11605 rexuz3 13404 smueqlem 14457 qnumdenbi 14686 dfiso3 15671 lssne0 18167 pjfval2 19265 0top 19992 1stccn 20471 dscopn 21581 bcthlem1 22285 ovolgelb 22426 iblpos 22743 itgposval 22746 itgsubstlem 22993 sincosq3sgn 23448 sincosq4sgn 23449 lgsquadlem3 24277 colinearalg 24933 wlklniswwlkn2 25421 rusgranumwlkb0 25674 usgreg2spot 25788 extwwlkfab 25811 numclwwlk2lem1 25823 nmoo0 26425 leop3 27771 leoptri 27782 f1od2 28302 tltnle 28416 nofulllem5 30588 dfrdg4 30711 poimirlem28 31961 itgaddnclem2 31994 lfl1dim 32681 glbconxN 32937 2dim 33029 elpadd0 33368 dalawlem13 33442 diclspsn 34756 dihglb2 34904 dochsordN 34936 lzunuz 35604 2reu4a 38604 funressnfv 38623 iccpartiltu 38730 |
Copyright terms: Public domain | W3C validator |