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 279 | . 2 ⊢ (𝜒 ↔ 𝜑) |
5 | 1, 4 | bitr3i 280 | 1 ⊢ (𝜃 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 |
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 210 |
This theorem is referenced by: nbbn 388 pm5.17 1012 dn1 1058 noranOLD 1533 dfeumo 2538 2ex2rexrot 3181 sbralie 3396 reu8 3663 sbcimdv 3786 sbcg 3791 unass 4097 ssin 4162 difab 4232 eq0rdv 4336 csbab 4369 ralidm 4440 iunssf 4970 iunss 4971 poirr 5498 elvvv 5642 cnvuni 5773 dfco2 6127 resin 6704 dffv2 6828 dff1o6 7108 fsplit 7907 sbthcl 8794 fiint 8978 rankf 9440 dfac3 9765 dfac5lem3 9769 elznn0 12221 elnn1uz2 12551 lsmspsn 20154 cmbr2i 29709 pjss2i 29793 iuninc 30651 fineqvrep 32808 dffr5 33471 elold 33824 brsset 33962 brtxpsd 33967 ellines 34225 itg2addnclem3 35604 dvasin 35635 cvlsupr3 37132 dihglb2 39130 ifpidg 40831 dfsucon 40863 iscard4 40873 ss2iundf 40992 dffrege76 41272 dffrege99 41295 ntrneikb 41429 disjinfi 42452 |
Copyright terms: Public domain | W3C validator |