![]() |
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 279 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
5 | 1, 4 | bitr3d 280 | 1 ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: rnmpt0f 6249 sbcoteq1a 8056 fnwelem 8136 mpocurryd 8275 compssiso 10404 divfl0 13830 cjreb 15114 cnpart 15231 bitsuz 16460 acsfn 17658 eqg0el 19163 ghmeqker 19223 odmulg 19540 psrbaglefi 21899 psrbaglefiOLD 21900 cnrest2 23251 hausdiag 23610 prdsbl 24461 mcubic 26844 2lgslem1a2 27388 fmptco1f1o 32519 qsidomlem2 33286 areacirclem4 37335 lmclim2 37382 cmtbr2N 38875 expdiophlem1 42589 cantnfresb 42900 rrx2linest 48006 |
Copyright terms: Public domain | W3C validator |