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-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: nbbn 347 pm5.17 858 dn1 932 sbralie 2848 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 6244 nclennlem1 6248 nnc3n3p1 6278 nchoicelem10 6298 nchoicelem16 6304 fnfreclem1 6317 |
Copyright terms: Public domain | W3C validator |