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  3084  sbcnel12g  3141  elxp4  5216  elxp5  5217  f1eq123d  5566  foeq123d  5567  f1oeq123d  5568  fnmptfvd  5741  ofrfval  6233  eloprabi  6348  fnmpoovd  6367  smoeq  6442  ecidg  6754  ixpsnval  6856  enqbreq2  7555  ltanqg  7598  caucvgprprlemexb  7905  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  ltrennb  8052  apneg  8769  mulext1  8770  apdivmuld  8971  ltdiv23  9050  lediv23  9051  halfpos  9353  addltmul  9359  div4p1lem1div2  9376  ztri3or  9500  supminfex  9804  iccf1o  10212  fzshftral  10316  fzoshftral  10456  infssuzex  10465  2tnp1ge0ge0  10533  fihashen1  11033  seq3coll  11077  s111  11179  swrdspsleq  11215  pfxeq  11244  wrd2ind  11271  cjap  11433  negfi  11755  tanaddaplem  12265  dvdssub  12365  addmodlteqALT  12386  dvdsmod  12389  oddp1even  12403  nn0o1gt2  12432  nn0oddm1d2  12436  bitscmp  12485  cncongr1  12641  cncongr2  12642  4sqlem11  12940  4sqlem17  12946  intopsn  13416  sgrp1  13460  sgrppropd  13462  issubg  13726  nmzsubg  13763  conjnmzb  13833  srg1zr  13966  ring1  14038  issubrg  14201  znf1o  14631  znleval  14633  znunit  14639  elmopn  15136  metss  15184  comet  15189  xmetxp  15197  limcmpted  15353  cnlimc  15362  lgsneg  15719  lgsne0  15733  lgsprme0  15737  lgsquadlem1  15772  lgsquadlem2  15773  2lgs  15799  2lgsoddprm  15808  edg0iedg0g  15882  wrdupgren  15912  wrdumgren  15922  vtxd0nedgbfi  16059