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  3367  elimhyp3v  3983  elimhyp4v  3984  keephyp3v  3989  opelopabgf  4753  f1eq123d  5797  foeq123d  5798  f1oeq123d  5799  fnmptfvd  5971  ofrfval  6529  eloprabi  6843  fnmpt2ovd  6859  suppsnop  6913  smoeq  7019  wemapwe  8137  wemapweOLD  8138  fseqenlem1  8403  dfac12lem2  8522  fin23lem22  8705  pwfseqlem5  9039  pwfseq  9040  enqbreq2  9296  lterpq  9346  ltdiv23  10437  lediv23  10438  halfpos  10770  addltmul  10775  supminf  11173  supxrbnd1  11517  supxrbnd2  11518  iccf1o  11668  fzshftral  11769  fzoshftral  11897  dfceil2  11942  modirr  12031  hashen1  12413  seqcoll  12486  s111  12597  swrdeq  12645  wrdeqswrdlsw  12648  wrd2ind  12677  2swrd2eqwrdeq  12865  limsupgle  13274  tanaddlem  13773  dvdssub  13898  dvdsmod  13915  oddp1even  13920  bitscmp  13960  saddisjlem  13986  smueqlem  14012  prmreclem5  14310  4sqlem11  14345  4sqlem17  14351  vdwmc2  14369  ismre  14859  acsfn  14928  isssc  15061  setcinv  15286  intopsn  15751  sgrp1  15787  mnd1OLD  15831  sgrp2nmndlem4  15915  nmzsubg  16111  conjnmzb  16170  gsmsymgreqlem2  16325  symgfixels  16328  f1omvdconj  16340  oddvdsnn0  16437  oddvds  16440  odcong  16442  odf1  16453  dpjeq  16976  dpjeqOLD  16983  pgpfac1lem2  16994  ring1  17116  lsmspsn  17598  lbsacsbs  17670  lpigen  17772  prmirredlem  18390  prmirredlemOLD  18393  znf1o  18457  znleval  18460  znunit  18469  islinds2  18715  islindf4  18740  scmatf1  18900  isclo  19454  maxlp  19514  1stccn  19830  xkoinjcn  20054  elmptrab  20194  fbunfip  20236  elfm  20314  fmid  20327  flfnei  20358  isflf  20360  isfcls  20376  fclsopn  20381  isfcf  20401  cnextfun  20430  eltsms  20497  prdsxmetlem  20737  elmopn  20811  metss  20877  comet  20882  elbl4  20945  metuel2  20948  nrmmetd  20961  metdsge  21219  tchcph  21546  fmcfil  21577  rrxmet  21701  minveclem4  21713  shft2rab  21785  sca2rab  21789  volsup2  21880  mbfsup  21937  i1fmullem  21967  mbfi1fseqlem4  21991  xrge0f  22004  itg2monolem1  22023  ellimc2  22147  cnlimc  22158  mdegleb  22330  facth1  22431  ulm2  22645  sineq0  22779  coseq1  22780  efeq1  22781  sinord  22786  root1eq1  22994  angrtmuld  23005  quad2  23035  dcubic  23042  cubic2  23044  dquartlem1  23047  dquart  23049  quart  23057  rlimcnp  23160  mumullem2  23319  chtub  23352  fsumvma  23353  fsumvma2  23354  chpchtsum  23359  bposlem7  23430  lgsneg  23459  lgsne0  23473  lgsqrlem2  23482  lgsquadlem1  23494  lgsquadlem2  23495  axcontlem7  24138  isuslgra  24208  isusgra  24209  ausisusgra  24220  nbgraopALT  24289  nb3graprlem2  24317  cusgra3v  24329  sizeusglecusg  24351  uvtx01vtx  24357  is2wlk  24432  0pth  24437  wlkdvspthlem  24474  2wlkeq  24572  wwlknextbi  24590  clwwlkn2  24640  el2wlkonotot0  24737  el2wlkonotot  24738  el2wlksoton  24743  el2spthsoton  24744  el2wlksot  24745  el2pthsot  24746  isrusgusrgcl  24798  rusgrasn  24810  rusgranumwlkl1  24812  rusgra0edg  24820  eupath2lem2  24843  eupath2lem3  24844  frgra2v  24864  frgra3v  24867  usg2spot2nb  24930  numclwwlkovfel2  24948  numclwwlk2lem1  24967  numclwlk2lem2f1o  24970  frgrareggt1  24981  isass  25183  rngosn3  25293  imsmetlem  25461  ipz  25497  bnsscmcl  25649  minvecolem4  25661  hvsubcan  25856  hoeq2  26615  leoptri  26920  atcv0eq  27163  elimifd  27286  gtiso  27384  2ndpreima  27390  fpwrelmapffslem  27420  fzsplit3  27464  isomnd  27557  ogrpinvlt  27580  pstmfval  27741  lmlim  27795  dya2ub  28107  eulerpartlemr  28179  isrrvv  28248  ballotlemsima  28320  signsvfn  28405  lgamucov  28446  subfacp1lem3  28492  subfacp1lem5  28494  erdszelem1  28501  erdsze  28512  erdsze2lem2  28514  elpredg  29226  dvtanlem  30032  itg2addnclem2  30035  ftc1anclem1  30058  areacirclem1  30075  areacirclem5  30079  filnetlem4  30167  metf1o  30216  elrfirn  30595  jm2.19lem2  30900  proot1ex  31130  fourierdlem113  31887  2reu4a  32028  ltnltne  32155  0nodd  32331  2nodd  32333  rngcinv  32508  rngcinvOLD  32520  ringcinv  32553  ringcinvOLD  32576  islindeps  32764  snlindsntor  32782  bj-issetwt  34147  bj-sbceqgALT  34181  lsatcv0eq  34474  cmtbr2N  34680  atlatmstc  34746  1cvrco  34898  cdleme3  35664  cdleme7  35676  cdlemg10c  36067  dvhopellsm  36546  dibord  36588  dib1dim2  36597  diblsmopel  36600  dihopelvalcpre  36677  dih1dimatlem  36758  hdmap14lem13  37312  hdmapoc  37363