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-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: an12 535 cbval2 1873 cbvex2 1874 sbco2v 1898 equsb3 1902 sbn 1903 sbim 1904 sbor 1905 sban 1906 sbco2h 1915 sbco2d 1917 sbco2vd 1918 sbcomv 1922 sbco3 1925 sbcom 1926 sbcom2v 1938 sbcom2v2 1939 sbcom2 1940 dfsb7 1944 sb7f 1945 sb7af 1946 sbal 1953 sbex 1957 sbco4lem 1959 moanim 2051 eq2tri 2177 eqsb3 2221 clelsb3 2222 clelsb4 2223 clelsb3f 2262 ralcom4 2682 rexcom4 2683 ceqsralt 2687 gencbvex 2706 gencbval 2708 ceqsrexbv 2790 euind 2844 reuind 2862 sbccomlem 2955 sbccom 2956 raaan 3439 elxp2 4527 eqbrriv 4604 dm0rn0 4726 dfres2 4841 qfto 4898 xpm 4930 rninxp 4952 fununi 5161 dfoprab2 5786 dfer2 6398 euen1 6664 xpsnen 6683 xpassen 6692 enq0enq 7207 prnmaxl 7264 prnminu 7265 suplocexprlemell 7489 |
Copyright terms: Public domain | W3C validator |