Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3bitrri | Structured version Visualization version GIF version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitri.1 | ⊢ (𝜑 ↔ 𝜓) |
3bitri.2 | ⊢ (𝜓 ↔ 𝜒) |
3bitri.3 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
3bitrri | ⊢ (𝜃 ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitri.3 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
2 | 3bitri.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 3bitri.2 | . . 3 ⊢ (𝜓 ↔ 𝜒) | |
4 | 2, 3 | bitr2i 277 | . 2 ⊢ (𝜒 ↔ 𝜑) |
5 | 1, 4 | bitr3i 278 | 1 ⊢ (𝜃 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ 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: nbbn 385 pm5.17 1005 dn1 1049 noranOLD 1518 2sb6rfOLD 2490 dfeumo 2612 2ex2rexrot 3247 sbralie 3469 reu8 3721 unass 4139 ssin 4204 difab 4269 csbab 4386 iunss 4960 poirr 5478 elvvv 5620 cnvuni 5750 dfco2 6091 resin 6629 dffv2 6749 dff1o6 7023 fsplit 7801 sbthcl 8627 fiint 8783 rankf 9211 dfac3 9535 dfac5lem3 9539 elznn0 11984 elnn1uz2 12313 lsmspsn 19785 cmbr2i 29300 pjss2i 29384 iuninc 30240 dffr5 32886 brsset 33247 brtxpsd 33252 ellines 33510 itg2addnclem3 34826 dvasin 34859 cvlsupr3 36360 dihglb2 38358 ifpidg 39735 dfsucon 39767 iscard4 39778 ss2iundf 39882 dffrege76 40163 dffrege99 40186 ntrneikb 40322 iunssf 41229 disjinfi 41330 |
Copyright terms: Public domain | W3C validator |