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

Theorem 3bitrd 213
Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)
Hypotheses
Ref Expression
3bitrd.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitrd.2  |-  ( ph  ->  ( ch  <->  th )
)
3bitrd.3  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
3bitrd  |-  ( ph  ->  ( ps  <->  ta )
)

Proof of Theorem 3bitrd
StepHypRef Expression
1 3bitrd.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 3bitrd.2 . . 3  |-  ( ph  ->  ( ch  <->  th )
)
31, 2bitrd 187 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitrd.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 187 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sbceqal  2916  sbcnel12g  2970  elxp4  4962  elxp5  4963  f1eq123d  5296  foeq123d  5297  f1oeq123d  5298  ofrfval  5922  eloprabi  6024  fnmpoovd  6042  smoeq  6117  ecidg  6423  ixpsnval  6525  enqbreq2  7066  ltanqg  7109  caucvgprprlemexb  7416  caucvgsrlemgt1  7490  caucvgsrlemoffres  7495  ltrennb  7541  apneg  8239  mulext1  8240  apdivmuld  8434  ltdiv23  8508  lediv23  8509  halfpos  8803  addltmul  8808  div4p1lem1div2  8825  ztri3or  8949  supminfex  9242  iccf1o  9628  fzshftral  9729  fzoshftral  9856  2tnp1ge0ge0  9915  fihashen1  10386  seq3coll  10426  cjap  10519  negfi  10838  tanaddaplem  11243  dvdssub  11333  addmodlteqALT  11352  dvdsmod  11355  oddp1even  11368  nn0o1gt2  11397  nn0oddm1d2  11401  infssuzex  11437  cncongr1  11577  cncongr2  11578  elmopn  12374  metss  12422  comet  12427
  Copyright terms: Public domain W3C validator