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

Theorem 3bitr3i 199
 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 175 . 2 (χψ)
4 3bitr3i.3 . 2 (ψθ)
53, 4bitri 173 1 (χθ)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  an12  495  cbval2  1793  cbvex2  1794  sbco2v  1818  equsb3  1822  sbn  1823  sbim  1824  sbor  1825  sban  1826  sbco2h  1835  sbco2d  1837  sbco2vd  1838  sbcomv  1842  sbco3  1845  sbcom  1846  sbcom2v  1858  sbcom2v2  1859  sbcom2  1860  dfsb7  1864  sb7f  1865  sb7af  1866  sbal  1873  sbex  1877  sbco4lem  1879  moanim  1971  eq2tri  2096  eqsb3  2138  clelsb3  2139  clelsb4  2140  ralcom4  2570  rexcom4  2571  ceqsralt  2575  gencbvex  2594  gencbval  2596  ceqsrexbv  2669  euind  2722  reuind  2738  sbccomlem  2826  sbccom  2827  raaan  3321  elxp2  4306  eqbrriv  4378  dm0rn0  4495  dfres2  4601  qfto  4657  xpm  4688  rninxp  4707  fununi  4910  dfoprab2  5494  dfer2  6043  euen1  6218  xpsnen  6231  xpassen  6240  enq0enq  6413  prnmaxl  6470  prnminu  6471
 Copyright terms: Public domain W3C validator