![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > bitrd | Unicode version |
Description: Deduction form of bitri 240. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.) |
Ref | Expression |
---|---|
bitrd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bitrd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bitrd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitrd.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | pm5.74i 236 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | bitrd.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | pm5.74i 236 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitri 240 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | pm5.74ri 237 |
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: bitr2d 245 bitr3d 246 bitr4d 247 syl5bb 248 syl6bb 252 3bitrd 270 3bitr2d 272 3bitr3d 274 3bitr4d 276 imbi12d 311 bibi12d 312 sylan9bb 680 orbi12d 690 anbi12d 691 dedlem0a 918 ax11el 2194 eleq12d 2421 neeq12d 2531 neleq12d 2609 raleqbi1dv 2815 rexeqbi1dv 2816 reueqd 2817 rmoeqd 2818 raleqbidv 2819 rexeqbidv 2820 raleqbidva 2821 rexeqbidva 2822 eueq3 3011 sbc19.21g 3110 sbcrext 3119 sbcabel 3123 sbcel1g 3155 sbceq1g 3156 sbcel2g 3157 sbceq2g 3158 sbccsb2g 3165 sbcco3g 3191 elin 3219 elun 3220 sseq12d 3300 psseq12d 3363 raaan 3657 raaanv 3658 sbcss 3660 elimhyp2v 3711 elimhyp4v 3713 keephyp2v 3717 ralsng 3765 rexsng 3766 ssunsn2 3865 2ralunsn 3880 csbunig 3899 otkelins2kg 4253 otkelins3kg 4254 opkelcokg 4261 opkelimagekg 4271 reiota2 4368 eqtfinrelk 4486 vfintle 4546 breq123d 4653 sbcbr12g 4686 sbcbr1g 4687 sbcbr2g 4688 csbxpg 4813 csbrng 4966 fneq12d 5177 feq12d 5216 f1osng 5323 csbfv12g 5336 eqfnfv2 5393 funimass3 5404 funconstss 5406 dffo3 5422 fressnfv 5439 f1elima 5474 isomin 5496 f1oiso 5499 ov 5595 ovg 5601 erth2 5969 elmapg 6012 elpmg 6013 ce0nnulb 6182 ce0lenc1 6239 nmembers1lem3 6270 nchoicelem8 6296 |
Copyright terms: Public domain | W3C validator |