|   | 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 276 | . 2 ⊢ (𝜒 ↔ 𝜑) | 
| 5 | 1, 4 | bitr3i 277 | 1 ⊢ (𝜃 ↔ 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 | 
| 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 207 | 
| This theorem is referenced by: nbbn 383 pm5.17 1013 dn1 1057 sb8v 2354 sb8f 2355 dfeumo 2536 2ex2rexrot 3297 sbralie 3357 sbralieALT 3358 ceqsralt 3515 reu8 3738 sbcimdv 3858 sbcg 3862 unass 4171 ssin 4238 difab 4309 eq0rdv 4406 csbab 4439 ralidm 4511 iunssf 5043 iunss 5044 poirr 5603 elvvv 5760 cnvuni 5896 dfco2 6264 resin 6869 dffv2 7003 dff1o6 7296 fsplit 8143 naddasslem1 8733 naddasslem2 8734 sbthcl 9136 fiint 9367 fiintOLD 9368 rankf 9835 dfac3 10162 dfac5lem3 10166 elznn0 12630 elnn1uz2 12968 lsmspsn 21084 elold 27909 elzs2 28386 cmbr2i 31616 pjss2i 31700 iuninc 32574 fineqvrep 35110 dffr5 35755 brsset 35891 brtxpsd 35896 ellines 36154 itg2addnclem3 37681 dvasin 37712 cvlsupr3 39346 dihglb2 41345 oneptri 43274 faosnf0.11b 43445 ifpidg 43509 dfsucon 43541 iscard4 43551 dffrege76 43957 dffrege99 43980 ntrneikb 44112 disjinfi 45202 | 
| Copyright terms: Public domain | W3C validator |