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  3006  sbcnel12g  3062  elxp4  5091  elxp5  5092  f1eq123d  5425  foeq123d  5426  f1oeq123d  5427  ofrfval  6058  eloprabi  6164  fnmpoovd  6183  smoeq  6258  ecidg  6565  ixpsnval  6667  enqbreq2  7298  ltanqg  7341  caucvgprprlemexb  7648  caucvgsrlemgt1  7736  caucvgsrlemoffres  7741  ltrennb  7795  apneg  8509  mulext1  8510  apdivmuld  8709  ltdiv23  8787  lediv23  8788  halfpos  9088  addltmul  9093  div4p1lem1div2  9110  ztri3or  9234  supminfex  9535  iccf1o  9940  fzshftral  10043  fzoshftral  10173  2tnp1ge0ge0  10236  fihashen1  10712  seq3coll  10755  cjap  10848  negfi  11169  tanaddaplem  11679  dvdssub  11778  addmodlteqALT  11797  dvdsmod  11800  oddp1even  11813  nn0o1gt2  11842  nn0oddm1d2  11846  infssuzex  11882  cncongr1  12035  cncongr2  12036  intopsn  12598  elmopn  13086  metss  13134  comet  13139  xmetxp  13147  limcmpted  13272  cnlimc  13281  lgsneg  13565  lgsne0  13579  lgsprme0  13583