![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > syl6ib | Unicode version |
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6ib.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl6ib.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl6ib |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6ib.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | syl6ib.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | biimpi 186 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl6 29 |
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: 3imtr3g 260 exp4a 589 mtord 641 19.23hOLD 1820 ax12olem6 1932 cbvexd 2009 ax15 2021 2eu3 2286 exists2 2294 necon2bd 2565 necon2d 2566 necon4ad 2577 necon4d 2579 necon1bd 2584 spcimgft 2930 eqsbc3r 3103 reupick 3539 evenodddisj 4516 sfinltfin 4535 vfin1cltv 4547 dmcosseq 4973 iss 5000 xp11 5056 ssrnres 5059 opelf 5235 mapsn 6026 |
Copyright terms: Public domain | W3C validator |