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  3084  sbcnel12g  3141  elxp4  5216  elxp5  5217  f1eq123d  5564  foeq123d  5565  f1oeq123d  5566  fnmptfvd  5739  ofrfval  6227  eloprabi  6342  fnmpoovd  6361  smoeq  6436  ecidg  6746  ixpsnval  6848  enqbreq2  7544  ltanqg  7587  caucvgprprlemexb  7894  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  ltrennb  8041  apneg  8758  mulext1  8759  apdivmuld  8960  ltdiv23  9039  lediv23  9040  halfpos  9342  addltmul  9348  div4p1lem1div2  9365  ztri3or  9489  supminfex  9792  iccf1o  10200  fzshftral  10304  fzoshftral  10444  infssuzex  10453  2tnp1ge0ge0  10521  fihashen1  11021  seq3coll  11064  s111  11164  swrdspsleq  11199  pfxeq  11228  wrd2ind  11255  cjap  11417  negfi  11739  tanaddaplem  12249  dvdssub  12349  addmodlteqALT  12370  dvdsmod  12373  oddp1even  12387  nn0o1gt2  12416  nn0oddm1d2  12420  bitscmp  12469  cncongr1  12625  cncongr2  12626  4sqlem11  12924  4sqlem17  12930  intopsn  13400  sgrp1  13444  sgrppropd  13446  issubg  13710  nmzsubg  13747  conjnmzb  13817  srg1zr  13950  ring1  14022  issubrg  14185  znf1o  14615  znleval  14617  znunit  14623  elmopn  15120  metss  15168  comet  15173  xmetxp  15181  limcmpted  15337  cnlimc  15346  lgsneg  15703  lgsne0  15717  lgsprme0  15721  lgsquadlem1  15756  lgsquadlem2  15757  2lgs  15783  2lgsoddprm  15792  edg0iedg0g  15866  wrdupgren  15896  wrdumgren  15906