![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > syl6rbbr | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
syl6rbbr.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl6rbbr.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl6rbbr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6rbbr.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | syl6rbbr.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | bicomi 193 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl6rbb 253 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: baib 871 reu8 3032 sbc6g 3071 r19.28z 3642 r19.28zv 3645 r19.37zv 3646 r19.45zv 3647 r19.27z 3648 r19.27zv 3649 r19.36zv 3650 ralidm 3653 ralsns 3763 rexsns 3764 ssunsn2 3865 iunconst 3977 iinconst 3978 ssofss 4076 snelpwg 4114 opres 4978 cores 5084 funssres 5144 fncnv 5158 dff1o5 5295 fvres 5342 funimass4 5368 dffo3 5422 funfvima 5459 eloprabga 5578 eqncg 6126 ncseqnc 6128 eqtc 6161 tcfnex 6244 nchoicelem11 6299 nchoicelem16 6304 nchoicelem18 6306 canncb 6332 |
Copyright terms: Public domain | W3C validator |