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  3088  sbcnel12g  3145  elxp4  5231  elxp5  5232  f1eq123d  5584  foeq123d  5585  f1oeq123d  5586  fnmptfvd  5760  ofrfval  6253  eloprabi  6370  fnmpoovd  6389  suppsnopdc  6428  smoeq  6499  ecidg  6811  ixpsnval  6913  enqbreq2  7637  ltanqg  7680  caucvgprprlemexb  7987  caucvgsrlemgt1  8075  caucvgsrlemoffres  8080  ltrennb  8134  apneg  8850  mulext1  8851  apdivmuld  9052  ltdiv23  9131  lediv23  9132  halfpos  9434  addltmul  9440  div4p1lem1div2  9457  ztri3or  9583  supminfex  9892  iccf1o  10301  fzshftral  10405  fzoshftral  10547  infssuzex  10556  2tnp1ge0ge0  10624  fihashen1  11124  seq3coll  11169  s111  11274  swrdspsleq  11314  pfxeq  11343  wrd2ind  11370  cjap  11546  negfi  11868  tanaddaplem  12379  dvdssub  12479  addmodlteqALT  12500  dvdsmod  12503  oddp1even  12517  nn0o1gt2  12546  nn0oddm1d2  12550  bitscmp  12599  cncongr1  12755  cncongr2  12756  4sqlem11  13054  4sqlem17  13060  intopsn  13530  sgrp1  13574  sgrppropd  13576  issubg  13840  nmzsubg  13877  conjnmzb  13947  srg1zr  14081  ring1  14153  issubrg  14316  znf1o  14747  znleval  14749  znunit  14755  elmopn  15257  metss  15305  comet  15310  xmetxp  15318  limcmpted  15474  cnlimc  15483  lgsneg  15843  lgsne0  15857  lgsprme0  15861  lgsquadlem1  15896  lgsquadlem2  15897  2lgs  15923  2lgsoddprm  15932  edg0iedg0g  16007  wrdupgren  16037  wrdumgren  16047  vtxd0nedgbfi  16240  eupth2lem2dc  16400  eupth2lem3lem6fi  16412  eupth2lem3lem4fi  16414