![]() |
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 185 | . 2 ⊢ (𝜒 ↔ 𝜓) |
4 | 3bitr3i.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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: an12 533 cbval2 1869 cbvex2 1870 sbco2v 1894 equsb3 1898 sbn 1899 sbim 1900 sbor 1901 sban 1902 sbco2h 1911 sbco2d 1913 sbco2vd 1914 sbcomv 1918 sbco3 1921 sbcom 1922 sbcom2v 1934 sbcom2v2 1935 sbcom2 1936 dfsb7 1940 sb7f 1941 sb7af 1942 sbal 1949 sbex 1953 sbco4lem 1955 moanim 2047 eq2tri 2172 eqsb3 2216 clelsb3 2217 clelsb4 2218 clelsb3f 2257 ralcom4 2677 rexcom4 2678 ceqsralt 2682 gencbvex 2701 gencbval 2703 ceqsrexbv 2784 euind 2838 reuind 2856 sbccomlem 2949 sbccom 2950 raaan 3433 elxp2 4515 eqbrriv 4592 dm0rn0 4714 dfres2 4827 qfto 4884 xpm 4916 rninxp 4938 fununi 5147 dfoprab2 5770 dfer2 6381 euen1 6647 xpsnen 6665 xpassen 6674 enq0enq 7180 prnmaxl 7237 prnminu 7238 |
Copyright terms: Public domain | W3C validator |