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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sbceqal  3107  sbcnel12g  3164  elxp4  5275  elxp5  5276  f1eq123d  5631  foeq123d  5632  f1oeq123d  5633  fnmptfvd  5813  ofrfval  6311  eloprabi  6432  fnmpoovd  6451  suppsnopdc  6490  smoeq  6561  ecidg  6873  ixpsnval  6983  mapsnend  7099  enqbreq2  7724  ltanqg  7767  caucvgprprlemexb  8074  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  ltrennb  8221  apneg  8941  mulext1  8942  apdivmuld  9145  ltdiv23  9224  lediv23  9225  halfpos  9540  addltmul  9546  div4p1lem1div2  9563  ztri3or  9691  supminfex  10006  iccf1o  10417  fzsplit3  10468  fzshftral  10525  fzoshftral  10667  infssuzex  10676  2tnp1ge0ge0  10749  fihashen1  11252  seq3coll  11308  s111  11413  swrdspsleq  11453  pfxeq  11482  wrd2ind  11509  cjap  11686  negfi  12009  tanaddaplem  12521  dvdssub  12621  addmodlteqALT  12642  dvdsmod  12645  oddp1even  12659  nn0o1gt2  12688  nn0oddm1d2  12692  bitscmp  12741  cncongr1  12897  cncongr2  12898  4sqlem11  13200  4sqlem17  13206  ballotfilemsima  13308  intopsn  13736  sgrp1  13775  sgrppropd  13777  issubg  14025  nmzsubg  14062  conjnmzb  14132  rng1zrlem  14307  ring1  14413  issubrg  14578  znf1o  15035  znleval  15037  znunit  15043  elmopn  15596  metss  15644  comet  15649  xmetxp  15657  limcmpted  15813  cnlimc  15822  lgsneg  16241  lgsne0  16255  lgsprme0  16259  lgsquadlem1  16294  lgsquadlem2  16295  2lgs  16321  2lgsoddprm  16330  edg0iedg0g  16405  wrdupgren  16435  wrdumgren  16445  vtxd0nedgbfi  16638  eupth2lem2dc  16798  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812