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

Theorem 3bitrd 213
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 187 . 2 (𝜑 → (𝜓𝜃))
4 3bitrd.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 187 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sbceqal  2936  sbcnel12g  2990  elxp4  4996  elxp5  4997  f1eq123d  5330  foeq123d  5331  f1oeq123d  5332  ofrfval  5958  eloprabi  6062  fnmpoovd  6080  smoeq  6155  ecidg  6461  ixpsnval  6563  enqbreq2  7133  ltanqg  7176  caucvgprprlemexb  7483  caucvgsrlemgt1  7571  caucvgsrlemoffres  7576  ltrennb  7630  apneg  8341  mulext1  8342  apdivmuld  8541  ltdiv23  8618  lediv23  8619  halfpos  8919  addltmul  8924  div4p1lem1div2  8941  ztri3or  9065  supminfex  9360  iccf1o  9755  fzshftral  9856  fzoshftral  9983  2tnp1ge0ge0  10042  fihashen1  10513  seq3coll  10553  cjap  10646  negfi  10967  tanaddaplem  11372  dvdssub  11465  addmodlteqALT  11484  dvdsmod  11487  oddp1even  11500  nn0o1gt2  11529  nn0oddm1d2  11533  infssuzex  11569  cncongr1  11711  cncongr2  11712  elmopn  12542  metss  12590  comet  12595  xmetxp  12603  limcmpted  12728  cnlimc  12737
  Copyright terms: Public domain W3C validator