Theorem 3bitr2d 296

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2d.1	|- ( ph -> ( ps <-> ch ) )
3bitr2d.2	|- ( ph -> ( th <-> ch ) )
3bitr2d.3	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
3bitr2d	|- ( ph -> ( ps <-> ta ) )

Proof of Theorem 3bitr2d

Step	Hyp	Ref	Expression
1		3bitr2d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		3bitr2d.2	. . 3 |- ( ph -> ( th <-> ch ) )
3	1, 2	bitr4d 271	. 2 |- ( ph -> ( ps <-> th ) )
4		3bitr2d.3	. 2 |- ( ph -> ( th <-> ta ) )
5	3, 4	bitrd 268	1 |- ( ph -> ( ps <-> ta ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  ceqsralt  3229  raltpd  4315  opiota  7229  adderpqlem  9776  mulerpqlem  9777  lesub2  10523  rec11  10723  avglt1  11270  ixxun  12191  modmuladdnn0  12714  hashdom  13168  hashle00  13188  hashf1lem1  13239  swrdspsleq  13449  repsdf2  13525  2shfti  13820  mulre  13861  rlim  14226  rlim2  14227  modremain  15132  nn0seqcvgd  15283  divgcdcoprm0  15379  prmreclem6  15625  pwsleval  16153  issubc  16495  ismgmid  17264  grpsubeq0  17501  grpsubadd  17503  gastacos  17743  orbsta  17746  lsslss  18961  coe1mul2lem1  19637  prmirredlem  19841  zndvds  19898  zntoslem  19905  cygznlem1  19915  islindf2  20153  restcld  20976  leordtvallem1  21014  leordtvallem2  21015  ist1-2  21151  xkoccn  21422  qtopcld  21516  ordthmeolem  21604  qustgpopn  21923  isxmet2d  22132  prdsxmetlem  22173  xblss2  22207  imasf1oxms  22294  neibl  22306  xrtgioo  22609  xrsxmet  22612  isncvsngp  22949  minveclem4  23203  minveclem6  23205  minveclem7  23206  mbfmulc2lem  23414  mbfmax  23416  mbfi1fseqlem4  23485  itg2gt0  23527  itg2cnlem2  23529  iblpos  23559  angrteqvd  24536  affineequiv  24553  affineequiv2  24554  dcubic  24573  rlimcnp  24692  rlimcnp2  24693  efexple  25006  bposlem7  25015  lgsabs1  25061  lgsquadlem1  25105  m1lgs  25113  lnhl  25510  colinearalg  25790  axcontlem2  25845  nbupgrel  26241  nb3grpr  26284  usgr0edg0rusgr  26471  isspthonpth  26645  rusgrnumwwlkl1  26863  eupth2lem3lem4  27091  numclwlk1lem2f1  27227  minvecolem4  27736  minvecolem6  27738  minvecolem7  27739  hvmulcan2  27930  xppreima  29449  smatrcl  29862  pstmxmet  29940  xrge0iifcnv  29979  ballotlemsima  30577  poimirlem27  33436  itg2addnclem  33461  itg2addnclem2  33462  iblabsnclem  33473  areacirclem2  33501  areacirclem4  33503  cvlcvrp  34627  ntrclsk2  38366  ntrclsk13  38369  ntrneixb  38393  neicvgel1  38417  radcnvrat  38513  mapsnend  39391  limsupmnflem  39952  logbge0b  42357