Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitrd 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  2814  sbcnel12g  2867  elxp4  4808  elxp5  4809  f1eq123d  5121  foeq123d  5122  f1oeq123d  5123  ofrfval  5720  eloprabi  5822  smoeq  5905  ecidg  6170  enqbreq2  6455  ltanqg  6498  caucvgprprlemexb  6805  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  ltrennb  6930  apneg  7602  mulext1  7603  ltdiv23  7858  lediv23  7859  halfpos  8156  addltmul  8161  div4p1lem1div2  8177  ztri3or  8288  iccf1o  8872  fzshftral  8970  fzoshftral  9094  2tnp1ge0ge0  9143  cjap  9506
 Copyright terms: Public domain W3C validator