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

Theorem 3bitrd 203
Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)
Hypotheses
Ref Expression
3bitrd.1
3bitrd.2
3bitrd.3
Assertion
Ref Expression
3bitrd

Proof of Theorem 3bitrd
StepHypRef Expression
1 3bitrd.1 . . 3
2 3bitrd.2 . . 3
31, 2bitrd 177 . 2
4 3bitrd.3 . 2
53, 4bitrd 177 1
Colors of variables: wff set class
Syntax hints:   wi 4   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:  sbceqal  2808  sbcnel12g  2861  elxp4  4751  elxp5  4752  f1eq123d  5064  foeq123d  5065  f1oeq123d  5066  ofrfval  5662  eloprabi  5764  smoeq  5846  ecidg  6106  enqbreq2  6341  ltanqg  6384  apneg  7395  mulext1  7396  ltdiv23  7639  lediv23  7640  halfpos  7933  addltmul  7938  ztri3or  8064  iccf1o  8642  fzshftral  8740  fzoshftral  8864  cjap  9134
  Copyright terms: Public domain W3C validator