New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > bitr4d | Unicode version |
Description: Deduction form of bitr4i 243. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr4d.1 | |
bitr4d.2 |
Ref | Expression |
---|---|
bitr4d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr4d.1 | . 2 | |
2 | bitr4d.2 | . . 3 | |
3 | 2 | bicomd 192 | . 2 |
4 | 1, 3 | bitrd 244 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 |
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 177 |
This theorem is referenced by: 3bitr2d 272 3bitr2rd 273 3bitr4d 276 3bitr4rd 277 bianabs 850 3anibar 1123 iota1 4353 lefinlteq 4463 funbrfv2b 5362 dffn5 5363 fnrnfv 5364 fniniseg 5371 dff13 5471 isoini 5497 caovord3 5631 ce0ncpw1 6185 cantcb 6335 |
Copyright terms: Public domain | W3C validator |