![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr3i | GIF version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.) |
Ref | Expression |
---|---|
3bitr3i.1 | ⊢ (𝜑 ↔ 𝜓) |
3bitr3i.2 | ⊢ (𝜑 ↔ 𝜒) |
3bitr3i.3 | ⊢ (𝜓 ↔ 𝜃) |
Ref | Expression |
---|---|
3bitr3i | ⊢ (𝜒 ↔ 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3i.2 | . . 3 ⊢ (𝜑 ↔ 𝜒) | |
2 | 3bitr3i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | bitr3i 184 | . 2 ⊢ (𝜒 ↔ 𝜓) |
4 | 3bitr3i.3 | . 2 ⊢ (𝜓 ↔ 𝜃) | |
5 | 3, 4 | bitri 182 | 1 ⊢ (𝜒 ↔ 𝜃) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: an12 526 cbval2 1839 cbvex2 1840 sbco2v 1864 equsb3 1868 sbn 1869 sbim 1870 sbor 1871 sban 1872 sbco2h 1881 sbco2d 1883 sbco2vd 1884 sbcomv 1888 sbco3 1891 sbcom 1892 sbcom2v 1904 sbcom2v2 1905 sbcom2 1906 dfsb7 1910 sb7f 1911 sb7af 1912 sbal 1919 sbex 1923 sbco4lem 1925 moanim 2017 eq2tri 2142 eqsb3 2186 clelsb3 2187 clelsb4 2188 ralcom4 2631 rexcom4 2632 ceqsralt 2636 gencbvex 2655 gencbval 2657 ceqsrexbv 2735 euind 2789 reuind 2805 sbccomlem 2898 sbccom 2899 raaan 3365 elxp2 4410 eqbrriv 4482 dm0rn0 4601 dfres2 4709 qfto 4765 xpm 4796 rninxp 4815 fununi 5019 dfoprab2 5605 dfer2 6196 euen1 6372 xpsnen 6388 xpassen 6397 enq0enq 6760 prnmaxl 6817 prnminu 6818 |
Copyright terms: Public domain | W3C validator |