Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3bitrrd | Structured version Visualization version GIF 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 281 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
5 | 1, 4 | bitr3d 282 | 1 ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: fnwelem 7814 mpocurryd 7924 compssiso 9784 divfl0 13182 cjreb 14470 cnpart 14587 bitsuz 15811 acsfn 16918 ghmeqker 18323 odmulg 18612 psrbaglefi 20080 cnrest2 21822 hausdiag 22181 prdsbl 23028 mcubic 25352 2lgslem1a2 25893 fmptco1f1o 30306 eqg0el 30853 qsidomlem2 30883 areacirclem4 34866 lmclim2 34914 cmtbr2N 36269 expdiophlem1 39496 rnmpt0 41359 rrx2linest 44657 |
Copyright terms: Public domain | W3C validator |