![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > bitr3d | Unicode version |
Description: Deduction form of bitr3i 242. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr3d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bitr3d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bitr3d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bicomd 192 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | bitr3d.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitrd 244 |
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: 3bitrrd 271 3bitr3d 274 3bitr3rd 275 biass 348 sbequ12a 1921 sbco2 2086 sbco3 2088 sbcom 2089 sb9i 2094 sbcom2 2114 sbal1 2126 sbal 2127 csbiebt 3172 opkelimagekg 4271 copsex2t 4608 copsex2g 4609 resieq 4979 fnssresb 5195 funimass5 5405 isocnv 5491 isoini 5497 ovmpt2x 5712 brcupg 5814 brcomposeg 5819 brcrossg 5848 enpw1 6062 enmap1lem3 6071 nenpw1pwlem2 6085 te0c 6237 |
Copyright terms: Public domain | W3C validator |