![]() |
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 278 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 3bitr2i.3 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
5 | 3, 4 | bitr2i 276 | 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 1515 ssrab 4035 copsex2gb 5767 relop 5811 dmopab3 5880 dfres2 6000 restidsing 6011 fununi 6581 dffv2 6941 dfsup2 9387 kmlem3 10095 recmulnq 10907 dmscut 27172 nbgrel 28330 shne0i 30432 13an22anass 31437 ssiun3 31519 cnvoprabOLD 31679 ind1a 32658 bnj1304 33471 bnj1253 33669 dfrecs2 34564 icorempo 35851 inxprnres 36782 disjressuc2 36879 dalem20 38185 ralopabb 41757 rp-isfinite6 41864 rababg 41920 ssrabf 43398 ralfal 43450 |
Copyright terms: Public domain | W3C validator |