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 281 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 3bitr2i.3 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
5 | 3, 4 | bitr2i 279 | 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: xorass 1512 nororOLD 1535 ssrab 3983 copsex2gb 5673 relop 5716 dmopab3 5785 dfres2 5906 restidsing 5919 fununi 6452 dffv2 6803 dfsup2 9057 kmlem3 9763 recmulnq 10575 nbgrel 27425 shne0i 29526 ssiun3 30614 cnvoprabOLD 30772 ind1a 31696 bnj1304 32509 bnj1253 32707 dmscut 33739 dfrecs2 33986 icorempo 35256 inxprnres 36162 dalem20 37442 rp-isfinite6 40808 rababg 40855 ssrabf 42335 |
Copyright terms: Public domain | W3C validator |