Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr3i GIF version

Theorem 3bitr3i 209
 Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
Hypotheses
Ref Expression
3bitr3i.1 (𝜑𝜓)
3bitr3i.2 (𝜑𝜒)
3bitr3i.3 (𝜓𝜃)
Assertion
Ref Expression
3bitr3i (𝜒𝜃)

Proof of Theorem 3bitr3i
StepHypRef Expression
1 3bitr3i.2 . . 3 (𝜑𝜒)
2 3bitr3i.1 . . 3 (𝜑𝜓)
31, 2bitr3i 185 . 2 (𝜒𝜓)
4 3bitr3i.3 . 2 (𝜓𝜃)
53, 4bitri 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  551  cbval2  1894  cbvex2  1895  sbco2vh  1919  equsb3  1925  sbn  1926  sbim  1927  sbor  1928  sban  1929  sbco2h  1938  sbco2d  1940  sbco2vd  1941  sbcomv  1945  sbco3  1948  sbcom  1949  sbcom2v  1961  sbcom2v2  1962  sbcom2  1963  dfsb7  1967  sb7f  1968  sb7af  1969  sbal  1976  sbex  1980  sbco4lem  1982  moanim  2074  eq2tri  2200  eqsb3  2244  clelsb3  2245  clelsb4  2246  clelsb3f  2286  ralcom4  2711  rexcom4  2712  ceqsralt  2716  gencbvex  2735  gencbval  2737  ceqsrexbv  2819  euind  2874  reuind  2892  sbccomlem  2986  sbccom  2987  raaan  3473  elxp2  4564  eqbrriv  4641  dm0rn0  4763  dfres2  4878  qfto  4935  xpm  4967  rninxp  4989  fununi  5198  dfoprab2  5825  dfer2  6437  euen1  6703  xpsnen  6722  xpassen  6731  enq0enq  7262  prnmaxl  7319  prnminu  7320  suplocexprlemell  7544
 Copyright terms: Public domain W3C validator