![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr4rd | Structured version Visualization version Unicode version |
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitr4d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3bitr4d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3bitr4d.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3bitr4rd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4d.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3bitr4d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitr4d 260 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr4d.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitr4d 260 |
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 189 |
This theorem is referenced by: inimasn 5256 oacan 7254 ecdmn0 7411 wemapwe 8207 r1pw 8321 adderpqlem 9384 mulerpqlem 9385 lterpq 9400 ltanq 9401 genpass 9439 readdcan 9812 lemuldiv 10493 msq11 10514 avglt2 10858 qbtwnre 11499 iooshf 11720 clim2c 13581 lo1o1 13608 climabs0 13661 reef11 14185 absefib 14264 efieq1re 14265 pc2dvds 14840 pcmpt 14849 subsubc 15770 odmulgid 17217 gexdvds 17247 submcmn2 17491 obslbs 19305 cnntr 20303 cndis 20319 cnindis 20320 cnpdis 20321 lmres 20328 cmpfi 20435 ist0-4 20756 txhmeo 20830 tsmssubm 21169 blin 21448 cncfmet 21952 icopnfcnv 21982 lmmbrf 22244 iscauf 22262 causs 22280 mbfposr 22620 itg2gt0 22730 limcflf 22848 limcres 22853 lhop1 22978 dvdsr1p 23124 fsumvma2 24154 vmasum 24156 chpchtsum 24159 bposlem1 24224 iscgrgd 24570 tgcgr4 24588 lnrot1 24680 eqeelen 24946 nbgraeledg 25170 nb3graprlem2 25192 cusgra3v 25204 cusgrauvtxb 25236 clwlkisclwwlk2 25530 el2spthonot0 25611 rusgranumwlks 25696 dmdmd 27965 funcnvmptOLD 28282 funcnvmpt 28283 1stpreimas 28298 xrdifh 28374 ismntop 28842 eulerpartlemgh 29223 signslema 29463 topdifinfindis 31761 leceifl 31946 iblabsnclem 32017 ftc1anclem6 32034 areacirclem5 32048 areacirc 32049 lsatfixedN 32587 cdlemg10c 34218 diaglbN 34635 dih1 34866 dihglbcpreN 34880 mapdcv 35240 ellz1 35621 islssfg 35940 proot1ex 36090 eliooshift 37614 clim2cf 37741 odd2np1ALTV 38813 nbusgreledg 39431 nb3grprlem2 39465 |
Copyright terms: Public domain | W3C validator |