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  2808  sbcnel12g  2861  elxp4  4751  elxp5  4752  f1eq123d  5064  foeq123d  5065  f1oeq123d  5066  ofrfval  5662  eloprabi  5764  smoeq  5846  ecidg  6106  enqbreq2  6341  ltanqg  6384  apneg  7395  mulext1  7396  ltdiv23  7639  lediv23  7640  halfpos  7933  addltmul  7938  ztri3or  8064  iccf1o  8642  fzshftral  8740  fzoshftral  8864  cjap  9134