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 556 cbval2 1914 cbvex2 1915 sbco2vh 1938 equsb3 1944 sbn 1945 sbim 1946 sbor 1947 sban 1948 sbco2h 1957 sbco2d 1959 sbco2vd 1960 sbcomv 1964 sbco3 1967 sbcom 1968 sbcom2v 1978 sbcom2v2 1979 sbcom2 1980 dfsb7 1984 sb7f 1985 sb7af 1986 sbal 1993 sbex 1997 sbco4lem 1999 moanim 2093 eq2tri 2230 eqsb1 2274 clelsb1 2275 clelsb2 2276 clelsb1f 2316 ralcom4 2752 rexcom4 2753 ceqsralt 2757 gencbvex 2776 gencbval 2778 ceqsrexbv 2861 euind 2917 reuind 2935 sbccomlem 3029 sbccom 3030 raaan 3521 elxp2 4629 eqbrriv 4706 dm0rn0 4828 dfres2 4943 qfto 5000 xpm 5032 rninxp 5054 fununi 5266 dfoprab2 5900 dfer2 6514 euen1 6780 xpsnen 6799 xpassen 6808 enq0enq 7393 prnmaxl 7450 prnminu 7451 suplocexprlemell 7675 |
Copyright terms: Public domain | W3C validator |