Theorem 3bitrd 203

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  sbceqal  2814  sbcnel12g  2867  elxp4  4808  elxp5  4809  f1eq123d  5121  foeq123d  5122  f1oeq123d  5123  ofrfval  5720  eloprabi  5822  smoeq  5905  ecidg  6170  enqbreq2  6455  ltanqg  6498  caucvgprprlemexb  6805  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  ltrennb  6930  apneg  7602  mulext1  7603  ltdiv23  7858  lediv23  7859  halfpos  8156  addltmul  8161  div4p1lem1div2  8177  ztri3or  8288  iccf1o  8872  fzshftral  8970  fzoshftral  9094  2tnp1ge0ge0  9143  cjap  9506