![]() |
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 186 | . 2 ⊢ (𝜒 ↔ 𝜓) |
4 | 3bitr3i.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: an12 561 cbval2 1933 cbvex2 1934 sbco2vh 1957 equsb3 1963 sbn 1964 sbim 1965 sbor 1966 sban 1967 sbco2h 1976 sbco2d 1978 sbco2vd 1979 sbcomv 1983 sbco3 1986 sbcom 1987 sbcom2v 1997 sbcom2v2 1998 sbcom2 1999 dfsb7 2003 sb7f 2004 sb7af 2005 sbal 2012 sbex 2016 sbco4lem 2018 moanim 2112 eq2tri 2249 eqsb1 2293 clelsb1 2294 clelsb2 2295 clelsb1f 2336 ralcom4 2774 rexcom4 2775 ceqsralt 2779 gencbvex 2798 gencbval 2800 ceqsrexbv 2883 euind 2939 reuind 2957 sbccomlem 3052 sbccom 3053 raaan 3544 elxp2 4662 eqbrriv 4739 dm0rn0 4862 dfres2 4977 qfto 5036 xpm 5068 rninxp 5090 fununi 5303 dfoprab2 5943 dfer2 6560 euen1 6828 xpsnen 6847 xpassen 6856 enq0enq 7460 prnmaxl 7517 prnminu 7518 suplocexprlemell 7742 |
Copyright terms: Public domain | W3C validator |