ILE Home 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  483  cbval2  1778  cbvex2  1779  sbco2v  1803  equsb3  1807  sbn  1808  sbim  1809  sbor  1810  sban  1811  sbco2h  1820  sbco2d  1822  sbco2vd  1823  sbcomv  1827  sbco3  1830  sbcom  1831  sbcom2v  1843  sbcom2v2  1844  sbcom2  1845  dfsb7  1849  sb7f  1850  sb7af  1851  sbal  1858  sbex  1862  sbco4lem  1864  moanim  1956  eq2tri  2081  eqsb3  2123  clelsb3  2124  clelsb4  2125  ralcom4  2553  rexcom4  2554  ceqsralt  2558  gencbvex  2577  gencbval  2579  ceqsrexbv  2652  euind  2705  reuind  2721  sbccomlem  2809  sbccom  2810  raaan  3306  elxp2  4290  eqbrriv  4362  dm0rn0  4479  dfres2  4585  qfto  4641  xpm  4672  rninxp  4691  fununi  4893  dfoprab2  5475  dfer2  6018  enq0enq  6286  prnmaxl  6342  prnminu  6343
  Copyright terms: Public domain W3C validator