Theorem 3bitrd 213

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 187	. 2 |- ( ph -> ( ps <-> th ) )
4		3bitrd.3	. 2 |- ( ph -> ( th <-> ta ) )
5	3, 4	bitrd 187	1 |- ( ph -> ( ps <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sbceqal  3010  sbcnel12g  3066  elxp4  5098  elxp5  5099  f1eq123d  5435  foeq123d  5436  f1oeq123d  5437  fnmptfvd  5600  ofrfval  6069  eloprabi  6175  fnmpoovd  6194  smoeq  6269  ecidg  6577  ixpsnval  6679  enqbreq2  7319  ltanqg  7362  caucvgprprlemexb  7669  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  ltrennb  7816  apneg  8530  mulext1  8531  apdivmuld  8730  ltdiv23  8808  lediv23  8809  halfpos  9109  addltmul  9114  div4p1lem1div2  9131  ztri3or  9255  supminfex  9556  iccf1o  9961  fzshftral  10064  fzoshftral  10194  2tnp1ge0ge0  10257  fihashen1  10734  seq3coll  10777  cjap  10870  negfi  11191  tanaddaplem  11701  dvdssub  11800  addmodlteqALT  11819  dvdsmod  11822  oddp1even  11835  nn0o1gt2  11864  nn0oddm1d2  11868  infssuzex  11904  cncongr1  12057  cncongr2  12058  intopsn  12621  sgrp1  12651  elmopn  13240  metss  13288  comet  13293  xmetxp  13301  limcmpted  13426  cnlimc  13435  lgsneg  13719  lgsne0  13733  lgsprme0  13737