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  3230  elimhyp3v  3838  elimhyp4v  3839  keephyp3v  3844  f1eq123d  5624  foeq123d  5625  f1oeq123d  5626  fnmptfvd  5794  ofrfval  6317  eloprabi  6625  fnmpt2ovd  6640  suppsnop  6693  smoeq  6797  wemapwe  7916  wemapweOLD  7917  fseqenlem1  8182  dfac12lem2  8301  fin23lem22  8484  pwfseqlem5  8818  pwfseq  8819  enqbreq2  9077  lterpq  9127  ltdiv23  10211  lediv23  10212  halfpos  10543  addltmul  10548  supminf  10930  supxrbnd1  11272  supxrbnd2  11273  iccf1o  11416  fzshftral  11531  fzoshftral  11620  dfceil2  11664  modirr  11753  seqcoll  12200  s111  12286  swrdeq  12324  wrdeqswrdlsw  12327  wrd2ind  12356  2swrd2eqwrdeq  12537  limsupgle  12939  tanaddlem  13433  dvdssub  13556  dvdsmod  13573  oddp1even  13577  bitscmp  13617  saddisjlem  13643  smueqlem  13669  prmreclem5  13964  4sqlem11  13999  4sqlem17  14005  vdwmc2  14023  ismre  14511  acsfn  14580  isssc  14716  setcinv  14941  nmzsubg  15702  conjnmzb  15761  gsmsymgreqlem2  15916  symgfixels  15919  f1omvdconj  15932  oddvdsnn0  16027  oddvds  16030  odcong  16032  odf1  16043  dpjeq  16532  dpjeqOLD  16539  pgpfac1lem2  16550  lsmspsn  17087  lbsacsbs  17159  lpigen  17260  prmirredlem  17759  prmirredlemOLD  17762  znf1o  17826  znleval  17829  znunit  17838  islinds2  18084  islindf4  18109  isclo  18533  maxlp  18593  1stccn  18909  xkoinjcn  19102  elmptrab  19242  fbunfip  19284  elfm  19362  fmid  19375  flfnei  19406  isflf  19408  isfcls  19424  fclsopn  19429  isfcf  19449  cnextfun  19478  eltsms  19545  prdsxmetlem  19785  elmopn  19859  metss  19925  comet  19930  elbl4  19993  metuel2  19996  nrmmetd  20009  metdsge  20267  tchcph  20594  fmcfil  20625  minveclem4  20761  shft2rab  20833  sca2rab  20837  volsup2  20927  mbfsup  20984  i1fmullem  21014  mbfi1fseqlem4  21038  xrge0f  21051  itg2monolem1  21070  ellimc2  21194  cnlimc  21205  mdegleb  21420  facth1  21521  ulm2  21735  sineq0  21868  coseq1  21869  efeq1  21870  sinord  21875  root1eq1  22078  angrtmuld  22089  quad2  22119  dcubic  22126  cubic2  22128  dquartlem1  22131  dquart  22133  quart  22141  rlimcnp  22244  mumullem2  22403  chtub  22436  fsumvma  22437  fsumvma2  22438  chpchtsum  22443  bposlem7  22514  lgsneg  22543  lgsne0  22557  lgsqrlem2  22566  lgsquadlem1  22578  lgsquadlem2  22579  axcontlem7  23039  isuslgra  23094  isusgra  23095  ausisusgra  23102  nb3graprlem2  23183  cusgra3v  23195  sizeusglecusg  23217  uvtx01vtx  23223  is2wlk  23287  0pth  23292  wlkdvspthlem  23329  eupath2lem2  23422  eupath2lem3  23423  isass  23626  rngosn3  23736  imsmetlem  23904  ipz  23940  bnsscmcl  24092  minvecolem4  24104  hvsubcan  24299  hoeq2  25058  leoptri  25363  atcv0eq  25606  elimifd  25729  gtiso  25820  2ndpreima  25826  fpwrelmapffslem  25857  fzsplit3  25901  isomnd  25988  ogrpinvlt  26011  pstmfval  26177  lmlim  26231  dya2ub  26539  eulerpartlemr  26605  isrrvv  26674  ballotlemsima  26746  signsvfn  26831  lgamucov  26872  subfacp1lem3  26918  subfacp1lem5  26920  erdszelem1  26927  erdsze  26938  erdsze2lem2  26940  elpredg  27486  dvtanlem  28285  itg2addnclem2  28288  ftc1anclem1  28311  areacirclem1  28328  areacirclem5  28332  filnetlem4  28446  metf1o  28495  elrfirn  28876  jm2.19lem2  29184  proot1ex  29414  2reu4a  29859  opelopabgf  29982  ltnltne  30022  2wlkeq  30134  wwlknextbi  30203  el2wlkonotot0  30237  el2wlkonotot  30238  el2wlksoton  30243  el2spthsoton  30244  el2wlksot  30245  el2pthsot  30246  clwwlkn2  30284  rusgrasn  30403  rusgranumwlkl1  30405  rusgra0edg  30419  frgra2v  30437  frgra3v  30440  usg2spot2nb  30504  numclwwlkovfel2  30522  numclwwlk2lem1  30541  numclwlk2lem2f1o  30544  frgrareggt1  30555  hashen1  30581  islindeps  30696  snlindsntor  30714  mnd1  30730  bj-sbceqgALT  31998  lsatcv0eq  32265  cmtbr2N  32471  atlatmstc  32537  1cvrco  32689  cdleme3  33454  cdleme7  33466  cdlemg10c  33856  dvhopellsm  34335  dibord  34377  dib1dim2  34386  diblsmopel  34389  dihopelvalcpre  34466  dih1dimatlem  34547  hdmap14lem13  35101  hdmapoc  35152