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  3018  sbcnel12g  3074  elxp4  5116  elxp5  5117  f1eq123d  5453  foeq123d  5454  f1oeq123d  5455  fnmptfvd  5620  ofrfval  6090  eloprabi  6196  fnmpoovd  6215  smoeq  6290  ecidg  6598  ixpsnval  6700  enqbreq2  7355  ltanqg  7398  caucvgprprlemexb  7705  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  ltrennb  7852  apneg  8567  mulext1  8568  apdivmuld  8769  ltdiv23  8848  lediv23  8849  halfpos  9149  addltmul  9154  div4p1lem1div2  9171  ztri3or  9295  supminfex  9596  iccf1o  10003  fzshftral  10107  fzoshftral  10237  2tnp1ge0ge0  10300  fihashen1  10778  seq3coll  10821  cjap  10914  negfi  11235  tanaddaplem  11745  dvdssub  11844  addmodlteqALT  11864  dvdsmod  11867  oddp1even  11880  nn0o1gt2  11909  nn0oddm1d2  11913  infssuzex  11949  cncongr1  12102  cncongr2  12103  intopsn  12785  sgrp1  12815  issubg  13031  nmzsubg  13068  srg1zr  13168  ring1  13234  issubrg  13340  elmopn  13916  metss  13964  comet  13969  xmetxp  13977  limcmpted  14102  cnlimc  14111  lgsneg  14395  lgsne0  14409  lgsprme0  14413