Theorem 3bitrd 212

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sbceqal  2869  sbcnel12g  2923  elxp4  4828  elxp5  4829  f1eq123d  5141  foeq123d  5142  f1oeq123d  5143  ofrfval  5740  eloprabi  5842  smoeq  5928  ecidg  6193  enqbreq2  6547  ltanqg  6590  caucvgprprlemexb  6897  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  ltrennb  7022  apneg  7711  mulext1  7712  ltdiv23  7970  lediv23  7971  halfpos  8262  addltmul  8267  div4p1lem1div2  8284  ztri3or  8394  supminfex  8685  iccf1o  9026  fzshftral  9125  fzoshftral  9247  2tnp1ge0ge0  9303  cjap  9793  negfi  10110  dvdssub  10240  addmodlteqALT  10259  dvdsmod  10262  oddp1even  10275  nn0o1gt2  10305  nn0oddm1d2  10309  infssuzex  10345  cncongr1  10485  cncongr2  10486