![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr2i | 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 |
---|---|
3bitr2i | ⊢ (φ ↔ θ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr2i.1 | . . 3 ⊢ (φ ↔ ψ) | |
2 | 3bitr2i.2 | . . 3 ⊢ (χ ↔ ψ) | |
3 | 1, 2 | bitr4i 176 | . 2 ⊢ (φ ↔ χ) |
4 | 3bitr2i.3 | . 2 ⊢ (χ ↔ θ) | |
5 | 3, 4 | bitri 173 | 1 ⊢ (φ ↔ θ) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: an13 497 sbanv 1766 sbexyz 1876 exists1 1993 euxfrdc 2721 euind 2722 rmo4 2728 rmo3 2843 opm 3962 uniuni 4149 rabxp 4323 eliunxp 4418 dmmrnm 4497 imadisj 4630 intirr 4654 resco 4768 funcnv3 4904 fncnv 4908 fun11 4909 fununi 4910 f1mpt 5353 mpt2mptx 5537 xpcomco 6236 enq0tr 6417 elq 8333 |
Copyright terms: Public domain | W3C validator |