![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > syl6bi | Unicode version |
Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.) |
Ref | Expression |
---|---|
syl6bi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl6bi.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl6bi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6bi.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpd 198 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | syl6bi.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 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: ax11i 1647 equveli 1988 eupickbi 2270 2eu2 2285 rgen2a 2680 reu6 3025 sseq0 3582 disjel 3597 disjpss 3601 uneqdifeq 3638 elinti 3935 pwadjoin 4119 preq12b 4127 nnsucelr 4428 sfindbl 4530 funimass2 5170 fconstfv 5456 oprabid 5550 enadj 6060 enpw1 6062 enprmaplem3 6078 nenpw1pwlem2 6085 1cnc 6139 ncspw1eu 6159 ce0nnulb 6182 letc 6231 ncslesuc 6267 nchoicelem3 6291 fnfreclem2 6318 fnfreclem3 6319 |
Copyright terms: Public domain | W3C validator |