![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bitr2d | Structured version Visualization version Unicode version |
Description: Deduction form of bitr2i 258. (Contributed by NM, 9-Jun-2004.) |
Ref | Expression |
---|---|
bitr2d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bitr2d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bitr2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr2d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | bitr2d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitrd 261 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | bicomd 206 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 |
This theorem is referenced by: 3bitrrd 288 3bitr2rd 290 pm5.18 362 ifptru 1446 sbequ12a 2095 elrnmpt1 5101 fndmdif 6008 weniso 6269 sbcopeq1a 6871 cfss 8720 posdif 10134 lesub1 10135 lesub0 10158 ltdivmul 10507 ledivmul 10508 zlem1lt 11016 zltlem1 11017 negelrp 11361 ioon0 11690 fzn 11843 fzrev2 11887 fz1sbc 11898 elfzp1b 11899 sumsqeq0 12384 hashfzdm 12644 hashfirdm 12646 fz1isolem 12656 sqrtle 13372 absgt0 13435 isershft 13775 incexc2 13944 dvdssubr 14394 gcdn0gt0 14534 pcfac 14892 ramval 15008 ramvalOLD 15009 ltbwe 18744 iunocv 19292 lmbrf 20324 perfcls 20429 ovolscalem1 22514 itg2mulclem 22752 sineq0 23524 efif1olem4 23542 atanord 23901 rlimcnp2 23940 bposlem7 24266 rpvmasum2 24398 trgcgrg 24608 legov3 24691 opphllem6 24842 ebtwntg 25060 wwlkm1edg 25511 usg2spthonot0 25665 hial2eq2 26808 adjsym 27534 cnvadj 27593 eigvalcl 27662 mddmd 28002 mdslmd2i 28031 elat2 28041 xdivpnfrp 28450 isorng 28610 unitdivcld 28755 indpreima 28894 iooscon 30018 possumd 30414 pdivsq 30433 poimirlem26 32010 areacirclem1 32076 isat3 32917 ishlat3N 32964 cvrval5 33024 llnexchb2 33478 lhpoc2N 33624 lhprelat3N 33649 lautcnvle 33698 lautcvr 33701 ltrncnvatb 33747 cdlemb3 34217 cdlemg17h 34279 dih0vbN 34894 djhcvat42 35027 dvh4dimat 35050 mapdordlem2 35249 diophun 35660 jm2.19lem4 35891 isrnghm 40164 lincfsuppcl 40478 logge0b 40614 loggt0b 40615 logle1b 40616 loglt1b 40617 |
Copyright terms: Public domain | W3C validator |