Theorem 3bitrd 214

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

Step	Hyp	Ref	Expression
1		3bitrd.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		3bitrd.2	. . 3 |- ( ph -> ( ch <-> th ) )
3	1, 2	bitrd 188	. 2 |- ( ph -> ( ps <-> th ) )
4		3bitrd.3	. 2 |- ( ph -> ( th <-> ta ) )
5	3, 4	bitrd 188	1 |- ( ph -> ( ps <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sbceqal  3041  sbcnel12g  3097  elxp4  5153  elxp5  5154  f1eq123d  5492  foeq123d  5493  f1oeq123d  5494  fnmptfvd  5662  ofrfval  6139  eloprabi  6249  fnmpoovd  6268  smoeq  6343  ecidg  6653  ixpsnval  6755  enqbreq2  7417  ltanqg  7460  caucvgprprlemexb  7767  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  ltrennb  7914  apneg  8630  mulext1  8631  apdivmuld  8832  ltdiv23  8911  lediv23  8912  halfpos  9213  addltmul  9219  div4p1lem1div2  9236  ztri3or  9360  supminfex  9662  iccf1o  10070  fzshftral  10174  fzoshftral  10305  2tnp1ge0ge0  10370  fihashen1  10870  seq3coll  10913  cjap  11050  negfi  11371  tanaddaplem  11881  dvdssub  11981  addmodlteqALT  12001  dvdsmod  12004  oddp1even  12017  nn0o1gt2  12046  nn0oddm1d2  12050  infssuzex  12086  cncongr1  12241  cncongr2  12242  4sqlem11  12539  4sqlem17  12545  intopsn  12950  sgrp1  12994  sgrppropd  12996  issubg  13243  nmzsubg  13280  conjnmzb  13350  srg1zr  13483  ring1  13555  issubrg  13717  znf1o  14139  znleval  14141  znunit  14147  elmopn  14614  metss  14662  comet  14667  xmetxp  14675  limcmpted  14817  cnlimc  14826  lgsneg  15140  lgsne0  15154  lgsprme0  15158  lgsquadlem1  15191