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