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  3054  sbcnel12g  3110  elxp4  5170  elxp5  5171  f1eq123d  5514  foeq123d  5515  f1oeq123d  5516  fnmptfvd  5684  ofrfval  6167  eloprabi  6282  fnmpoovd  6301  smoeq  6376  ecidg  6686  ixpsnval  6788  enqbreq2  7470  ltanqg  7513  caucvgprprlemexb  7820  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  ltrennb  7967  apneg  8684  mulext1  8685  apdivmuld  8886  ltdiv23  8965  lediv23  8966  halfpos  9268  addltmul  9274  div4p1lem1div2  9291  ztri3or  9415  supminfex  9718  iccf1o  10126  fzshftral  10230  fzoshftral  10367  infssuzex  10376  2tnp1ge0ge0  10444  fihashen1  10944  seq3coll  10987  s111  11085  swrdspsleq  11120  cjap  11217  negfi  11539  tanaddaplem  12049  dvdssub  12149  addmodlteqALT  12170  dvdsmod  12173  oddp1even  12187  nn0o1gt2  12216  nn0oddm1d2  12220  bitscmp  12269  cncongr1  12425  cncongr2  12426  4sqlem11  12724  4sqlem17  12730  intopsn  13199  sgrp1  13243  sgrppropd  13245  issubg  13509  nmzsubg  13546  conjnmzb  13616  srg1zr  13749  ring1  13821  issubrg  13983  znf1o  14413  znleval  14415  znunit  14421  elmopn  14918  metss  14966  comet  14971  xmetxp  14979  limcmpted  15135  cnlimc  15144  lgsneg  15501  lgsne0  15515  lgsprme0  15519  lgsquadlem1  15554  lgsquadlem2  15555  2lgs  15581  2lgsoddprm  15590