Theorem 3bitrd 213

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 187	. 2 |- ( ph -> ( ps <-> th ) )
4		3bitrd.3	. 2 |- ( ph -> ( th <-> ta ) )
5	3, 4	bitrd 187	1 |- ( ph -> ( ps <-> ta ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sbceqal  2916  sbcnel12g  2970  elxp4  4962  elxp5  4963  f1eq123d  5296  foeq123d  5297  f1oeq123d  5298  ofrfval  5922  eloprabi  6024  fnmpoovd  6042  smoeq  6117  ecidg  6423  ixpsnval  6525  enqbreq2  7066  ltanqg  7109  caucvgprprlemexb  7416  caucvgsrlemgt1  7490  caucvgsrlemoffres  7495  ltrennb  7541  apneg  8239  mulext1  8240  apdivmuld  8434  ltdiv23  8508  lediv23  8509  halfpos  8803  addltmul  8808  div4p1lem1div2  8825  ztri3or  8949  supminfex  9242  iccf1o  9628  fzshftral  9729  fzoshftral  9856  2tnp1ge0ge0  9915  fihashen1  10386  seq3coll  10426  cjap  10519  negfi  10838  tanaddaplem  11243  dvdssub  11333  addmodlteqALT  11352  dvdsmod  11355  oddp1even  11368  nn0o1gt2  11397  nn0oddm1d2  11401  infssuzex  11437  cncongr1  11577  cncongr2  11578  elmopn  12374  metss  12422  comet  12427