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-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  8340  mulext1  8341  apdivmuld  8540  ltdiv23  8614  lediv23  8615  halfpos  8909  addltmul  8914  div4p1lem1div2  8931  ztri3or  9055  supminfex  9348  iccf1o  9742  fzshftral  9843  fzoshftral  9970  2tnp1ge0ge0  10029  fihashen1  10500  seq3coll  10540  cjap  10633  negfi  10954  tanaddaplem  11359  dvdssub  11450  addmodlteqALT  11469  dvdsmod  11472  oddp1even  11485  nn0o1gt2  11514  nn0oddm1d2  11518  infssuzex  11554  cncongr1  11696  cncongr2  11697  elmopn  12526  metss  12574  comet  12579  xmetxp  12587  limcmpted  12712  cnlimc  12721
  Copyright terms: Public domain W3C validator