ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitrd Structured version   GIF 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  7355  mulext1  7356  ltdiv23  7599  lediv23  7600  halfpos  7893  addltmul  7898  ztri3or  8024  iccf1o  8602  fzshftral  8700  fzoshftral  8824  cjap  9094
  Copyright terms: Public domain W3C validator