Theorem 3bitrd 283

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

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

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 189

This theorem is referenced by:  sbceqal  3352  elimhyp3v  3970  elimhyp4v  3971  keephyp3v  3976  opelopabgf  4738  elpredg  5411  f1eq123d  5824  foeq123d  5825  f1oeq123d  5826  fnmptfvd  5998  ofrfval  6551  eloprabi  6867  fnmpt2ovd  6883  suppsnop  6937  smoeq  7075  infglbb  8011  wemapwe  8205  fseqenlem1  8457  dfac12lem2  8576  fin23lem22  8759  pwfseqlem5  9090  pwfseq  9091  enqbreq2  9347  lterpq  9397  ltdiv23  10499  lediv23  10500  negfi  10556  halfpos  10845  addltmul  10850  supminf  11252  supminfOLD  11253  supxrbnd1  11609  supxrbnd2  11610  iccf1o  11778  fzshftral  11884  fzoshftral  12023  dfceil2  12069  modirr  12161  hashen1  12551  seqcoll  12626  s111  12748  swrdeq  12796  wrd2ind  12830  2swrd2eqwrdeq  13022  limsupgle  13528  tanaddlem  14213  dvdssub  14338  dvdsmod  14355  oddp1even  14360  bitscmp  14405  saddisjlem  14431  smueqlem  14457  ncoprmgcdne1b  14648  prmreclem5  14857  4sqlem11  14892  4sqlem17OLD  14898  4sqlem17  14904  vdwmc2  14922  ismre  15489  acsfn  15558  dfiso2  15670  brcic  15696  isssc  15718  setcinv  15978  intopsn  16491  sgrp1  16527  mnd1OLD  16571  sgrp2nmndlem4  16655  nmzsubg  16851  conjnmzb  16910  gsmsymgreqlem2  17065  symgfixels  17068  f1omvdconj  17080  oddvdsnn0  17186  oddvds  17189  odcong  17191  odf1  17206  dpjeq  17685  pgpfac1lem2  17701  ring1  17823  lsmspsn  18300  lbsacsbs  18372  lpigen  18473  prmirredlem  19056  znf1o  19114  znleval  19117  znunit  19126  islinds2  19363  islindf4  19388  scmatf1  19548  isclo  20095  maxlp  20155  1stccn  20470  xkoinjcn  20694  elmptrab  20834  fbunfip  20876  elfm  20954  fmid  20967  flfnei  20998  isflf  21000  isfcls  21016  fclsopn  21021  isfcf  21041  cnextfun  21071  eltsms  21139  prdsxmetlem  21375  elmopn  21449  metss  21515  comet  21520  elbl4  21570  metuel2  21572  nrmmetd  21581  metdsge  21858  metdsgeOLD  21873  tchcph  22203  fmcfil  22234  rrxmet  22354  minveclem4  22366  minveclem4OLD  22378  shft2rab  22453  sca2rab  22457  volsup2  22555  mbfsup  22612  i1fmullem  22644  mbfi1fseqlem4  22668  xrge0f  22681  itg2monolem1  22700  ellimc2  22824  cnlimc  22835  mdegleb  23005  facth1  23107  ulm2  23332  sineq0  23468  coseq1  23469  efeq1  23470  sinord  23475  root1eq1  23687  angrtmuld  23729  quad2  23757  dcubic  23764  cubic2  23766  dquartlem1  23769  dquart  23771  quart  23779  rlimcnp  23883  lgamucov  23955  mumullem2  24099  chtub  24132  fsumvma  24133  fsumvma2  24134  chpchtsum  24139  bposlem7  24210  lgsneg  24239  lgsne0  24253  lgsqrlem2  24262  lgsquadlem1  24274  lgsquadlem2  24275  istrkg3ld  24501  tgcgr4  24568  iscgra1  24844  isleag  24875  iseqlg  24889  axcontlem7  24992  isuslgra  25062  isusgra  25063  ausisusgra  25074  nbgraopALT  25144  nb3graprlem2  25172  cusgra3v  25184  sizeusglecusg  25206  uvtx01vtx  25212  is2wlk  25287  0pth  25292  wlkdvspthlem  25329  2wlkeq  25427  wwlknextbi  25445  clwwlkn2  25495  el2wlkonotot0  25592  el2wlkonotot  25593  el2wlksoton  25598  el2spthsoton  25599  el2wlksot  25600  el2pthsot  25601  isrusgusrgcl  25653  rusgrasn  25665  rusgranumwlkl1  25667  rusgra0edg  25675  eupath2lem2  25698  eupath2lem3  25699  frgra2v  25719  frgra3v  25722  usg2spot2nb  25785  numclwwlkovfel2  25803  numclwwlk2lem1  25822  numclwlk2lem2f1o  25825  frgrareggt1  25836  isass  26036  rngosn3  26146  imsmetlem  26314  ipz  26350  bnsscmcl  26502  minvecolem4  26514  minvecolem4OLD  26524  hvsubcan  26719  hoeq2  27476  leoptri  27781  atcv0eq  28024  elimifd  28156  gtiso  28277  2ndpreima  28284  fpwrelmapffslem  28317  fzsplit3  28370  isomnd  28465  ogrpinvlt  28488  smatrcl  28624  pstmfval  28701  lmlim  28755  dya2ub  29094  eulerpartlemr  29209  isrrvv  29278  ballotlemsima  29350  ballotlemsimaOLD  29388  signsvfn  29473  subfacp1lem3  29907  subfacp1lem5  29909  erdszelem1  29916  erdsze  29927  erdsze2lem2  29929  filnetlem4  31036  bj-issetwt  31432  bj-sbceqgALT  31467  csbwrecsg  31686  poimirlem24  31922  dvtanlemOLD  31949  itg2addnclem2  31952  ftc1anclem1  31975  areacirclem1  31990  areacirclem5  31994  metf1o  32042  lsatcv0eq  32576  cmtbr2N  32782  atlatmstc  32848  1cvrco  33000  cdleme3  33766  cdleme7  33778  cdlemg10c  34169  dvhopellsm  34648  dibord  34690  dib1dim2  34699  diblsmopel  34702  dihopelvalcpre  34779  dih1dimatlem  34860  hdmap14lem13  35414  hdmapoc  35465  elrfirn  35500  jm2.19lem2  35809  pwfi2f1o  35918  proot1ex  36042  brfvidRP  36184  bcc0  36591  pwpwuni  37303  rnmptpr  37337  disjinfi  37362  fourierdlem113  37947  2reu4a  38367  iccpartgtl  38496  iccpartleu  38498  iccpartgel  38499  bits0ALTV  38564  bgoldbtbndlem1  38656  pfxeq  38701  ltnltne  38778  ausgrusgrb  38924  0nodd  39152  2nodd  39154  rngcinv  39325  rngcinvALTV  39337  ringcinv  39376  ringcinvALTV  39400  islindeps  39590  snlindsntor  39608  nn0o1gt2  39671  blen1b  39743  nn0sumshdiglem1  39776