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  2870  sbcnel12g  2924  elxp4  4838  elxp5  4839  f1eq123d  5152  foeq123d  5153  f1oeq123d  5154  ofrfval  5751  eloprabi  5853  smoeq  5939  ecidg  6236  enqbreq2  6609  ltanqg  6652  caucvgprprlemexb  6959  caucvgsrlemgt1  7033  caucvgsrlemoffres  7038  ltrennb  7084  apneg  7778  mulext1  7779  ltdiv23  8037  lediv23  8038  halfpos  8329  addltmul  8334  div4p1lem1div2  8351  ztri3or  8475  supminfex  8766  iccf1o  9102  fzshftral  9201  fzoshftral  9324  2tnp1ge0ge0  9383  sizeen1  9823  cjap  9931  negfi  10248  dvdssub  10385  addmodlteqALT  10404  dvdsmod  10407  oddp1even  10420  nn0o1gt2  10449  nn0oddm1d2  10453  infssuzex  10489  cncongr1  10629  cncongr2  10630