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  3019  sbcnel12g  3075  elxp4  5117  elxp5  5118  f1eq123d  5454  foeq123d  5455  f1oeq123d  5456  fnmptfvd  5621  ofrfval  6091  eloprabi  6197  fnmpoovd  6216  smoeq  6291  ecidg  6599  ixpsnval  6701  enqbreq2  7356  ltanqg  7399  caucvgprprlemexb  7706  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  ltrennb  7853  apneg  8568  mulext1  8569  apdivmuld  8770  ltdiv23  8849  lediv23  8850  halfpos  9150  addltmul  9155  div4p1lem1div2  9172  ztri3or  9296  supminfex  9597  iccf1o  10004  fzshftral  10108  fzoshftral  10238  2tnp1ge0ge0  10301  fihashen1  10779  seq3coll  10822  cjap  10915  negfi  11236  tanaddaplem  11746  dvdssub  11845  addmodlteqALT  11865  dvdsmod  11868  oddp1even  11881  nn0o1gt2  11910  nn0oddm1d2  11914  infssuzex  11950  cncongr1  12103  cncongr2  12104  intopsn  12786  sgrp1  12816  issubg  13033  nmzsubg  13070  srg1zr  13170  ring1  13236  issubrg  13342  elmopn  13949  metss  13997  comet  14002  xmetxp  14010  limcmpted  14135  cnlimc  14144  lgsneg  14428  lgsne0  14442  lgsprme0  14446