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

Theorem 3bitrd 207
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 181 . 2 (𝜑 → (𝜓𝜃))
4 3bitrd.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 181 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  sbceqal  2841  sbcnel12g  2895  elxp4  4836  elxp5  4837  f1eq123d  5149  foeq123d  5150  f1oeq123d  5151  ofrfval  5748  eloprabi  5850  smoeq  5936  ecidg  6201  enqbreq2  6513  ltanqg  6556  caucvgprprlemexb  6863  caucvgsrlemgt1  6937  caucvgsrlemoffres  6942  ltrennb  6988  apneg  7676  mulext1  7677  ltdiv23  7933  lediv23  7934  halfpos  8213  addltmul  8218  div4p1lem1div2  8235  ztri3or  8345  iccf1o  8973  fzshftral  9072  fzoshftral  9196  2tnp1ge0ge0  9251  cjap  9734  dvdssub  10152  addmodlteqALT  10171  dvdsmod  10174  oddp1even  10187  nn0o1gt2  10217  nn0oddm1d2  10221
  Copyright terms: Public domain W3C validator