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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sbceqal  3001  sbcnel12g  3057  elxp4  5085  elxp5  5086  f1eq123d  5419  foeq123d  5420  f1oeq123d  5421  ofrfval  6052  eloprabi  6156  fnmpoovd  6174  smoeq  6249  ecidg  6556  ixpsnval  6658  enqbreq2  7289  ltanqg  7332  caucvgprprlemexb  7639  caucvgsrlemgt1  7727  caucvgsrlemoffres  7732  ltrennb  7786  apneg  8500  mulext1  8501  apdivmuld  8700  ltdiv23  8778  lediv23  8779  halfpos  9079  addltmul  9084  div4p1lem1div2  9101  ztri3or  9225  supminfex  9526  iccf1o  9931  fzshftral  10033  fzoshftral  10163  2tnp1ge0ge0  10226  fihashen1  10701  seq3coll  10741  cjap  10834  negfi  11155  tanaddaplem  11665  dvdssub  11763  addmodlteqALT  11782  dvdsmod  11785  oddp1even  11798  nn0o1gt2  11827  nn0oddm1d2  11831  infssuzex  11867  cncongr1  12014  cncongr2  12015  elmopn  12987  metss  13035  comet  13040  xmetxp  13048  limcmpted  13173  cnlimc  13182