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  8939  mulext1  8940  apdivmuld  9143  ltdiv23  9222  lediv23  9223  halfpos  9536  addltmul  9542  div4p1lem1div2  9559  ztri3or  9687  supminfex  9997  iccf1o  10407  fzsplit3  10458  fzshftral  10515  fzoshftral  10657  infssuzex  10666  2tnp1ge0ge0  10736  fihashen1  11238  seq3coll  11294  s111  11399  swrdspsleq  11439  pfxeq  11468  wrd2ind  11495  cjap  11672  negfi  11994  tanaddaplem  12505  dvdssub  12605  addmodlteqALT  12626  dvdsmod  12629  oddp1even  12643  nn0o1gt2  12672  nn0oddm1d2  12676  bitscmp  12725  cncongr1  12881  cncongr2  12882  4sqlem11  13180  4sqlem17  13186  ballotfilemsima  13259  intopsn  13687  sgrp1  13726  sgrppropd  13728  issubg  13976  nmzsubg  14013  conjnmzb  14083  rng1zrlem  14258  ring1  14364  issubrg  14529  znf1o  14986  znleval  14988  znunit  14994  elmopn  15547  metss  15595  comet  15600  xmetxp  15608  limcmpted  15764  cnlimc  15773  lgsneg  16143  lgsne0  16157  lgsprme0  16161  lgsquadlem1  16196  lgsquadlem2  16197  2lgs  16223  2lgsoddprm  16232  edg0iedg0g  16307  wrdupgren  16337  wrdumgren  16347  vtxd0nedgbfi  16540  eupth2lem2dc  16700  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714