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 186 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 3bitr2i.3 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
5 | 3, 4 | bitri 183 | 1 ⊢ (𝜑 ↔ 𝜃) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: an13 558 sbanv 1882 sbexyz 1996 exists1 2115 euxfrdc 2916 euind 2917 rmo4 2923 rmo3f 2927 rmo3 3046 ddifstab 3259 opm 4217 uniuni 4434 rabxp 4646 eliunxp 4748 dmmrnm 4828 imadisj 4971 intirr 4995 resco 5113 funcnv3 5258 fncnv 5262 fun11 5263 fununi 5264 f1mpt 5748 mpomptx 5942 ixp0x 6702 mapsnen 6787 xpcomco 6802 enq0tr 7389 elq 9574 pythagtrip 12230 ntreq0 12891 tx1cn 13028 |
Copyright terms: Public domain | W3C validator |