Theorem 3bitrd 279

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

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

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 185

This theorem is referenced by:  sbceqal  3237  elimhyp3v  3845  elimhyp4v  3846  keephyp3v  3851  f1eq123d  5631  foeq123d  5632  f1oeq123d  5633  fnmptfvd  5801  ofrfval  6323  eloprabi  6631  fnmpt2ovd  6646  suppsnop  6699  smoeq  6803  wemapwe  7920  wemapweOLD  7921  fseqenlem1  8186  dfac12lem2  8305  fin23lem22  8488  pwfseqlem5  8822  pwfseq  8823  enqbreq2  9081  lterpq  9131  ltdiv23  10215  lediv23  10216  halfpos  10547  addltmul  10552  supminf  10934  supxrbnd1  11276  supxrbnd2  11277  iccf1o  11421  fzshftral  11539  fzoshftral  11628  dfceil2  11672  modirr  11761  seqcoll  12208  s111  12294  swrdeq  12332  wrdeqswrdlsw  12335  wrd2ind  12364  2swrd2eqwrdeq  12545  limsupgle  12947  tanaddlem  13442  dvdssub  13565  dvdsmod  13582  oddp1even  13586  bitscmp  13626  saddisjlem  13652  smueqlem  13678  prmreclem5  13973  4sqlem11  14008  4sqlem17  14014  vdwmc2  14032  ismre  14520  acsfn  14589  isssc  14725  setcinv  14950  nmzsubg  15713  conjnmzb  15772  gsmsymgreqlem2  15927  symgfixels  15930  f1omvdconj  15943  oddvdsnn0  16038  oddvds  16041  odcong  16043  odf1  16054  dpjeq  16546  dpjeqOLD  16553  pgpfac1lem2  16564  lsmspsn  17142  lbsacsbs  17214  lpigen  17315  prmirredlem  17892  prmirredlemOLD  17895  znf1o  17959  znleval  17962  znunit  17971  islinds2  18217  islindf4  18242  isclo  18666  maxlp  18726  1stccn  19042  xkoinjcn  19235  elmptrab  19375  fbunfip  19417  elfm  19495  fmid  19508  flfnei  19539  isflf  19541  isfcls  19557  fclsopn  19562  isfcf  19582  cnextfun  19611  eltsms  19678  prdsxmetlem  19918  elmopn  19992  metss  20058  comet  20063  elbl4  20126  metuel2  20129  nrmmetd  20142  metdsge  20400  tchcph  20727  fmcfil  20758  minveclem4  20894  shft2rab  20966  sca2rab  20970  volsup2  21060  mbfsup  21117  i1fmullem  21147  mbfi1fseqlem4  21171  xrge0f  21184  itg2monolem1  21203  ellimc2  21327  cnlimc  21338  mdegleb  21510  facth1  21611  ulm2  21825  sineq0  21958  coseq1  21959  efeq1  21960  sinord  21965  root1eq1  22168  angrtmuld  22179  quad2  22209  dcubic  22216  cubic2  22218  dquartlem1  22221  dquart  22223  quart  22231  rlimcnp  22334  mumullem2  22493  chtub  22526  fsumvma  22527  fsumvma2  22528  chpchtsum  22533  bposlem7  22604  lgsneg  22633  lgsne0  22647  lgsqrlem2  22656  lgsquadlem1  22668  lgsquadlem2  22669  axcontlem7  23167  isuslgra  23222  isusgra  23223  ausisusgra  23230  nb3graprlem2  23311  cusgra3v  23323  sizeusglecusg  23345  uvtx01vtx  23351  is2wlk  23415  0pth  23420  wlkdvspthlem  23457  eupath2lem2  23550  eupath2lem3  23551  isass  23754  rngosn3  23864  imsmetlem  24032  ipz  24068  bnsscmcl  24220  minvecolem4  24232  hvsubcan  24427  hoeq2  25186  leoptri  25491  atcv0eq  25734  elimifd  25856  gtiso  25947  2ndpreima  25953  fpwrelmapffslem  25983  fzsplit3  26029  isomnd  26115  ogrpinvlt  26138  pstmfval  26275  lmlim  26329  dya2ub  26637  eulerpartlemr  26709  isrrvv  26778  ballotlemsima  26850  signsvfn  26935  lgamucov  26976  subfacp1lem3  27022  subfacp1lem5  27024  erdszelem1  27031  erdsze  27042  erdsze2lem2  27044  elpredg  27590  dvtanlem  28394  itg2addnclem2  28397  ftc1anclem1  28420  areacirclem1  28437  areacirclem5  28441  filnetlem4  28555  metf1o  28604  elrfirn  28984  jm2.19lem2  29292  proot1ex  29522  2reu4a  29966  opelopabgf  30089  ltnltne  30129  2wlkeq  30241  wwlknextbi  30310  el2wlkonotot0  30344  el2wlkonotot  30345  el2wlksoton  30350  el2spthsoton  30351  el2wlksot  30352  el2pthsot  30353  clwwlkn2  30391  rusgrasn  30510  rusgranumwlkl1  30512  rusgra0edg  30526  frgra2v  30544  frgra3v  30547  usg2spot2nb  30611  numclwwlkovfel2  30629  numclwwlk2lem1  30648  numclwlk2lem2f1o  30651  frgrareggt1  30662  hashen1  30689  islindeps  30876  snlindsntor  30894  mnd1  30910  bj-issetwt  32219  bj-sbceqgALT  32253  lsatcv0eq  32532  cmtbr2N  32738  atlatmstc  32804  1cvrco  32956  cdleme3  33721  cdleme7  33733  cdlemg10c  34123  dvhopellsm  34602  dibord  34644  dib1dim2  34653  diblsmopel  34656  dihopelvalcpre  34733  dih1dimatlem  34814  hdmap14lem13  35368  hdmapoc  35419