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 1769 sbexyz 1879 exists1 1996 euxfrdc 2727 euind 2728 rmo4 2734 rmo3 2849 opm 3971 uniuni 4183 rabxp 4380 eliunxp 4475 dmmrnm 4554 imadisj 4687 intirr 4711 resco 4825 funcnv3 4961 fncnv 4965 fun11 4966 fununi 4967 f1mpt 5410 mpt2mptx 5595 xpcomco 6300 enq0tr 6532 elq 8557 |
Copyright terms: Public domain | W3C validator |