Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr3i Unicode 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  1796  cbvex2  1797  sbco2v  1821  equsb3  1825  sbn  1826  sbim  1827  sbor  1828  sban  1829  sbco2h  1838  sbco2d  1840  sbco2vd  1841  sbcomv  1845  sbco3  1848  sbcom  1849  sbcom2v  1861  sbcom2v2  1862  sbcom2  1863  dfsb7  1867  sb7f  1868  sb7af  1869  sbal  1876  sbex  1880  sbco4lem  1882  moanim  1974  eq2tri  2099  eqsb3  2141  clelsb3  2142  clelsb4  2143  ralcom4  2576  rexcom4  2577  ceqsralt  2581  gencbvex  2600  gencbval  2602  ceqsrexbv  2675  euind  2728  reuind  2744  sbccomlem  2832  sbccom  2833  raaan  3327  elxp2  4363  eqbrriv  4435  dm0rn0  4552  dfres2  4658  qfto  4714  xpm  4745  rninxp  4764  fununi  4967  dfoprab2  5552  dfer2  6107  euen1  6282  xpsnen  6295  xpassen  6304  enq0enq  6529  prnmaxl  6586  prnminu  6587
 Copyright terms: Public domain W3C validator