Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3bitrrd | Structured version Visualization version Unicode version |
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitrd.1 | |
3bitrd.2 | |
3bitrd.3 |
Ref | Expression |
---|---|
3bitrrd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitrd.3 | . 2 | |
2 | 3bitrd.1 | . . 3 | |
3 | 3bitrd.2 | . . 3 | |
4 | 2, 3 | bitr2d 269 | . 2 |
5 | 1, 4 | bitr3d 270 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 |
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 197 |
This theorem is referenced by: fnwelem 7292 mpt2curryd 7395 compssiso 9196 divfl0 12625 cjreb 13863 cnpart 13980 bitsuz 15196 acsfn 16320 ghmeqker 17687 odmulg 17973 psrbaglefi 19372 cnrest2 21090 hausdiag 21448 prdsbl 22296 mcubic 24574 2lgslem1a2 25115 fmptco1f1o 29434 areacirclem4 33503 lmclim2 33554 cmtbr2N 34540 expdiophlem1 37588 rnmpt0 39412 |
Copyright terms: Public domain | W3C validator |