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  3107  sbcnel12g  3164  elxp4  5270  elxp5  5271  f1eq123d  5626  foeq123d  5627  f1oeq123d  5628  fnmptfvd  5804  ofrfval  6301  eloprabi  6422  fnmpoovd  6441  suppsnopdc  6480  smoeq  6551  ecidg  6863  ixpsnval  6973  mapsnend  7089  enqbreq2  7714  ltanqg  7757  caucvgprprlemexb  8064  caucvgsrlemgt1  8152  caucvgsrlemoffres  8157  ltrennb  8211  apneg  8929  mulext1  8930  apdivmuld  9133  ltdiv23  9212  lediv23  9213  halfpos  9515  addltmul  9521  div4p1lem1div2  9538  ztri3or  9666  supminfex  9976  iccf1o  10386  fzsplit3  10436  fzshftral  10493  fzoshftral  10635  infssuzex  10644  2tnp1ge0ge0  10714  fihashen1  11216  seq3coll  11272  s111  11377  swrdspsleq  11417  pfxeq  11446  wrd2ind  11473  cjap  11650  negfi  11972  tanaddaplem  12483  dvdssub  12583  addmodlteqALT  12604  dvdsmod  12607  oddp1even  12621  nn0o1gt2  12650  nn0oddm1d2  12654  bitscmp  12703  cncongr1  12859  cncongr2  12860  4sqlem11  13158  4sqlem17  13164  ballotfilemsima  13237  intopsn  13664  sgrp1  13703  sgrppropd  13705  issubg  13953  nmzsubg  13990  conjnmzb  14060  rng1zrlem  14233  ring1  14337  issubrg  14502  znf1o  14958  znleval  14960  znunit  14966  elmopn  15470  metss  15518  comet  15523  xmetxp  15531  limcmpted  15687  cnlimc  15696  lgsneg  16057  lgsne0  16071  lgsprme0  16075  lgsquadlem1  16110  lgsquadlem2  16111  2lgs  16137  2lgsoddprm  16146  edg0iedg0g  16221  wrdupgren  16251  wrdumgren  16261  vtxd0nedgbfi  16454  eupth2lem2dc  16614  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628