Theorem 3bitrd 214

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sbceqal  3033  sbcnel12g  3089  elxp4  5134  elxp5  5135  f1eq123d  5472  foeq123d  5473  f1oeq123d  5474  fnmptfvd  5641  ofrfval  6115  eloprabi  6221  fnmpoovd  6240  smoeq  6315  ecidg  6625  ixpsnval  6727  enqbreq2  7386  ltanqg  7429  caucvgprprlemexb  7736  caucvgsrlemgt1  7824  caucvgsrlemoffres  7829  ltrennb  7883  apneg  8598  mulext1  8599  apdivmuld  8800  ltdiv23  8879  lediv23  8880  halfpos  9180  addltmul  9185  div4p1lem1div2  9202  ztri3or  9326  supminfex  9627  iccf1o  10034  fzshftral  10138  fzoshftral  10268  2tnp1ge0ge0  10332  fihashen1  10811  seq3coll  10854  cjap  10947  negfi  11268  tanaddaplem  11778  dvdssub  11877  addmodlteqALT  11897  dvdsmod  11900  oddp1even  11913  nn0o1gt2  11942  nn0oddm1d2  11946  infssuzex  11982  cncongr1  12135  cncongr2  12136  4sqlem11  12433  4sqlem17  12439  intopsn  12843  sgrp1  12874  sgrppropd  12876  issubg  13112  nmzsubg  13149  conjnmzb  13219  srg1zr  13341  ring1  13411  issubrg  13568  elmopn  14406  metss  14454  comet  14459  xmetxp  14467  limcmpted  14592  cnlimc  14601  lgsneg  14886  lgsne0  14900  lgsprme0  14904