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

Theorem 3bitrd 212
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 186 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitrd.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 186 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sbceqal  2870  sbcnel12g  2924  elxp4  4838  elxp5  4839  f1eq123d  5152  foeq123d  5153  f1oeq123d  5154  ofrfval  5751  eloprabi  5853  smoeq  5939  ecidg  6236  enqbreq2  6609  ltanqg  6652  caucvgprprlemexb  6959  caucvgsrlemgt1  7033  caucvgsrlemoffres  7038  ltrennb  7084  apneg  7778  mulext1  7779  ltdiv23  8037  lediv23  8038  halfpos  8329  addltmul  8334  div4p1lem1div2  8351  ztri3or  8475  supminfex  8766  iccf1o  9102  fzshftral  9201  fzoshftral  9324  2tnp1ge0ge0  9383  sizeen1  9823  cjap  9931  negfi  10248  dvdssub  10385  addmodlteqALT  10404  dvdsmod  10407  oddp1even  10420  nn0o1gt2  10449  nn0oddm1d2  10453  infssuzex  10489  cncongr1  10629  cncongr2  10630
  Copyright terms: Public domain W3C validator