![]() |
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 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 7337 mpt2curryd 7440 compssiso 9234 divfl0 12665 cjreb 13907 cnpart 14024 bitsuz 15243 acsfn 16367 ghmeqker 17734 odmulg 18019 psrbaglefi 19420 cnrest2 21138 hausdiag 21496 prdsbl 22343 mcubic 24619 2lgslem1a2 25160 fmptco1f1o 29562 areacirclem4 33633 lmclim2 33684 cmtbr2N 34858 expdiophlem1 37905 rnmpt0 39726 |
Copyright terms: Public domain | W3C validator |