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  3061  sbcnel12g  3118  elxp4  5189  elxp5  5190  f1eq123d  5536  foeq123d  5537  f1oeq123d  5538  fnmptfvd  5707  ofrfval  6190  eloprabi  6305  fnmpoovd  6324  smoeq  6399  ecidg  6709  ixpsnval  6811  enqbreq2  7505  ltanqg  7548  caucvgprprlemexb  7855  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  ltrennb  8002  apneg  8719  mulext1  8720  apdivmuld  8921  ltdiv23  9000  lediv23  9001  halfpos  9303  addltmul  9309  div4p1lem1div2  9326  ztri3or  9450  supminfex  9753  iccf1o  10161  fzshftral  10265  fzoshftral  10404  infssuzex  10413  2tnp1ge0ge0  10481  fihashen1  10981  seq3coll  11024  s111  11123  swrdspsleq  11158  pfxeq  11187  wrd2ind  11214  cjap  11332  negfi  11654  tanaddaplem  12164  dvdssub  12264  addmodlteqALT  12285  dvdsmod  12288  oddp1even  12302  nn0o1gt2  12331  nn0oddm1d2  12335  bitscmp  12384  cncongr1  12540  cncongr2  12541  4sqlem11  12839  4sqlem17  12845  intopsn  13314  sgrp1  13358  sgrppropd  13360  issubg  13624  nmzsubg  13661  conjnmzb  13731  srg1zr  13864  ring1  13936  issubrg  14098  znf1o  14528  znleval  14530  znunit  14536  elmopn  15033  metss  15081  comet  15086  xmetxp  15094  limcmpted  15250  cnlimc  15259  lgsneg  15616  lgsne0  15630  lgsprme0  15634  lgsquadlem1  15669  lgsquadlem2  15670  2lgs  15696  2lgsoddprm  15705  edg0iedg0g  15777  wrdupgren  15807  wrdumgren  15817