New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3bitrri | 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 241 | . 2 ⊢ (χ ↔ φ) |
5 | 1, 4 | bitr3i 242 | 1 ⊢ (θ ↔ φ) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: nbbn 347 pm5.17 858 dn1 932 reu8 3032 unass 3420 ssin 3477 difab 3523 iunss 4007 insklem 4304 eqpw1relk 4479 eqtfinrelk 4486 nnadjoin 4520 cnvuni 4895 dfco2 5080 resin 5307 dff1o6 5475 txpcofun 5803 releqel 5807 fnfullfunlem1 5856 ovcelem1 6171 tcfnex 6243 nclennlem1 6247 nnc3n3p1 6276 nchoicelem10 6296 nchoicelem16 6302 fnfreclem1 6315 |
Copyright terms: Public domain | W3C validator |