![]() |
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 187 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 3bitr2i.3 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
5 | 3, 4 | bitri 184 | 1 ⊢ (𝜑 ↔ 𝜃) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: an13 563 sbanv 1901 sbexyz 2019 exists1 2138 euxfrdc 2947 euind 2948 rmo4 2954 rmo3f 2958 rmo3 3078 ddifstab 3292 opm 4264 uniuni 4483 rabxp 4697 eliunxp 4802 dmmrnm 4882 imadisj 5028 intirr 5053 resco 5171 funcnv3 5317 fncnv 5321 fun11 5322 fununi 5323 f1mpt 5815 mpomptx 6010 ixp0x 6782 mapsnen 6867 xpcomco 6882 enq0tr 7496 elq 9690 pythagtrip 12424 ntreq0 14311 tx1cn 14448 |
Copyright terms: Public domain | W3C validator |