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  3016  sbcnel12g  3072  elxp4  5108  elxp5  5109  f1eq123d  5445  foeq123d  5446  f1oeq123d  5447  fnmptfvd  5612  ofrfval  6081  eloprabi  6187  fnmpoovd  6206  smoeq  6281  ecidg  6589  ixpsnval  6691  enqbreq2  7331  ltanqg  7374  caucvgprprlemexb  7681  caucvgsrlemgt1  7769  caucvgsrlemoffres  7774  ltrennb  7828  apneg  8542  mulext1  8543  apdivmuld  8743  ltdiv23  8822  lediv23  8823  halfpos  9123  addltmul  9128  div4p1lem1div2  9145  ztri3or  9269  supminfex  9570  iccf1o  9975  fzshftral  10078  fzoshftral  10208  2tnp1ge0ge0  10271  fihashen1  10747  seq3coll  10790  cjap  10883  negfi  11204  tanaddaplem  11714  dvdssub  11813  addmodlteqALT  11832  dvdsmod  11835  oddp1even  11848  nn0o1gt2  11877  nn0oddm1d2  11881  infssuzex  11917  cncongr1  12070  cncongr2  12071  intopsn  12661  sgrp1  12691  srg1zr  12976  ring1  13041  elmopn  13526  metss  13574  comet  13579  xmetxp  13587  limcmpted  13712  cnlimc  13721  lgsneg  14005  lgsne0  14019  lgsprme0  14023