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  2964  sbcnel12g  3019  elxp4  5029  elxp5  5030  f1eq123d  5363  foeq123d  5364  f1oeq123d  5365  ofrfval  5993  eloprabi  6097  fnmpoovd  6115  smoeq  6190  ecidg  6496  ixpsnval  6598  enqbreq2  7184  ltanqg  7227  caucvgprprlemexb  7534  caucvgsrlemgt1  7622  caucvgsrlemoffres  7627  ltrennb  7681  apneg  8392  mulext1  8393  apdivmuld  8592  ltdiv23  8669  lediv23  8670  halfpos  8970  addltmul  8975  div4p1lem1div2  8992  ztri3or  9116  supminfex  9414  iccf1o  9810  fzshftral  9912  fzoshftral  10039  2tnp1ge0ge0  10098  fihashen1  10569  seq3coll  10609  cjap  10702  negfi  11023  tanaddaplem  11468  dvdssub  11561  addmodlteqALT  11580  dvdsmod  11583  oddp1even  11596  nn0o1gt2  11625  nn0oddm1d2  11629  infssuzex  11665  cncongr1  11807  cncongr2  11808  elmopn  12641  metss  12689  comet  12694  xmetxp  12702  limcmpted  12827  cnlimc  12836
  Copyright terms: Public domain W3C validator