Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3bitr2ri | Structured version Visualization version GIF version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitr2i.1 | ⊢ (𝜑 ↔ 𝜓) |
3bitr2i.2 | ⊢ (𝜒 ↔ 𝜓) |
3bitr2i.3 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
3bitr2ri | ⊢ (𝜃 ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 3bitr2i.2 | . . 3 ⊢ (𝜒 ↔ 𝜓) | |
3 | 1, 2 | bitr4i 267 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 3bitr2i.3 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
5 | 3, 4 | bitr2i 265 | 1 ⊢ (𝜃 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ 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: xorass 1468 ssrab 3680 copsex2gb 5230 relop 5272 dmopab3 5337 restidsing 5458 issref 5509 fununi 5964 dffv2 6271 dfsup2 8350 kmlem3 8974 recmulnq 9786 ovoliunlem1 23270 shne0i 28307 ssiun3 29376 cnvoprab 29498 ind1a 30081 bnj1304 30890 bnj1253 31085 dmscut 31918 dfrecs2 32057 icorempt2 33199 inxprnres 34060 dalem20 34979 rp-isfinite6 37864 rababg 37879 ssrabf 39298 |
Copyright terms: Public domain | W3C validator |