ILE Home 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  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