![]() |
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 277 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 3bitr2i.3 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
5 | 3, 4 | bitr2i 275 | 1 ⊢ (𝜃 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ 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: xorass 1509 ssrab 4066 copsex2gb 5804 relop 5849 dmopab3 5918 dfres2 6042 restidsing 6054 fununi 6626 dffv2 6989 dfsup2 9480 kmlem3 10188 recmulnq 10998 dmscut 27838 nbgrel 29273 shne0i 31378 13an22anass 32391 ssiun3 32479 cnvoprabOLD 32634 ind1a 33865 bnj1304 34677 bnj1253 34875 dfrecs2 35787 icorempo 37071 inxprnres 38003 disjressuc2 38099 dalem20 39405 ralopabb 43115 rp-isfinite6 43222 rababg 43278 ssrabf 44752 ralfal 44802 |
Copyright terms: Public domain | W3C validator |