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  3350  elimhyp3v  3959  elimhyp4v  3960  keephyp3v  3965  f1eq123d  5745  foeq123d  5746  f1oeq123d  5747  fnmptfvd  5916  ofrfval  6439  eloprabi  6747  fnmpt2ovd  6762  suppsnop  6815  smoeq  6922  wemapwe  8040  wemapweOLD  8041  fseqenlem1  8306  dfac12lem2  8425  fin23lem22  8608  pwfseqlem5  8942  pwfseq  8943  enqbreq2  9201  lterpq  9251  ltdiv23  10335  lediv23  10336  halfpos  10667  addltmul  10672  supminf  11054  supxrbnd1  11396  supxrbnd2  11397  iccf1o  11547  fzshftral  11665  fzoshftral  11754  dfceil2  11798  modirr  11887  hashen1  12255  seqcoll  12335  s111  12421  swrdeq  12459  wrdeqswrdlsw  12462  wrd2ind  12491  2swrd2eqwrdeq  12672  limsupgle  13074  tanaddlem  13569  dvdssub  13692  dvdsmod  13709  oddp1even  13713  bitscmp  13753  saddisjlem  13779  smueqlem  13805  prmreclem5  14100  4sqlem11  14135  4sqlem17  14141  vdwmc2  14159  ismre  14648  acsfn  14717  isssc  14853  setcinv  15078  nmzsubg  15842  conjnmzb  15901  gsmsymgreqlem2  16056  symgfixels  16059  f1omvdconj  16072  oddvdsnn0  16169  oddvds  16172  odcong  16174  odf1  16185  dpjeq  16681  dpjeqOLD  16688  pgpfac1lem2  16699  lsmspsn  17289  lbsacsbs  17361  lpigen  17462  prmirredlem  18043  prmirredlemOLD  18046  znf1o  18110  znleval  18113  znunit  18122  islinds2  18368  islindf4  18393  isclo  18824  maxlp  18884  1stccn  19200  xkoinjcn  19393  elmptrab  19533  fbunfip  19575  elfm  19653  fmid  19666  flfnei  19697  isflf  19699  isfcls  19715  fclsopn  19720  isfcf  19740  cnextfun  19769  eltsms  19836  prdsxmetlem  20076  elmopn  20150  metss  20216  comet  20221  elbl4  20284  metuel2  20287  nrmmetd  20300  metdsge  20558  tchcph  20885  fmcfil  20916  minveclem4  21052  shft2rab  21124  sca2rab  21128  volsup2  21219  mbfsup  21276  i1fmullem  21306  mbfi1fseqlem4  21330  xrge0f  21343  itg2monolem1  21362  ellimc2  21486  cnlimc  21497  mdegleb  21669  facth1  21770  ulm2  21984  sineq0  22117  coseq1  22118  efeq1  22119  sinord  22124  root1eq1  22327  angrtmuld  22338  quad2  22368  dcubic  22375  cubic2  22377  dquartlem1  22380  dquart  22382  quart  22390  rlimcnp  22493  mumullem2  22652  chtub  22685  fsumvma  22686  fsumvma2  22687  chpchtsum  22692  bposlem7  22763  lgsneg  22792  lgsne0  22806  lgsqrlem2  22815  lgsquadlem1  22827  lgsquadlem2  22828  axcontlem7  23369  isuslgra  23424  isusgra  23425  ausisusgra  23432  nb3graprlem2  23513  cusgra3v  23525  sizeusglecusg  23547  uvtx01vtx  23553  is2wlk  23617  0pth  23622  wlkdvspthlem  23659  eupath2lem2  23752  eupath2lem3  23753  isass  23956  rngosn3  24066  imsmetlem  24234  ipz  24270  bnsscmcl  24422  minvecolem4  24434  hvsubcan  24629  hoeq2  25388  leoptri  25693  atcv0eq  25936  elimifd  26057  gtiso  26148  2ndpreima  26154  fpwrelmapffslem  26184  fzsplit3  26224  isomnd  26310  ogrpinvlt  26333  pstmfval  26469  lmlim  26523  dya2ub  26830  eulerpartlemr  26902  isrrvv  26971  ballotlemsima  27043  signsvfn  27128  lgamucov  27169  subfacp1lem3  27215  subfacp1lem5  27217  erdszelem1  27224  erdsze  27235  erdsze2lem2  27237  elpredg  27784  dvtanlem  28590  itg2addnclem2  28593  ftc1anclem1  28616  areacirclem1  28633  areacirclem5  28637  filnetlem4  28751  metf1o  28800  elrfirn  29180  jm2.19lem2  29488  proot1ex  29718  2reu4a  30162  opelopabgf  30285  ltnltne  30325  2wlkeq  30437  wwlknextbi  30506  el2wlkonotot0  30540  el2wlkonotot  30541  el2wlksoton  30546  el2spthsoton  30547  el2wlksot  30548  el2pthsot  30549  clwwlkn2  30587  rusgrasn  30706  rusgranumwlkl1  30708  rusgra0edg  30722  frgra2v  30740  frgra3v  30743  usg2spot2nb  30807  numclwwlkovfel2  30825  numclwwlk2lem1  30844  numclwlk2lem2f1o  30847  frgrareggt1  30858  islindeps  31120  snlindsntor  31138  mnd1  31154  bj-issetwt  32703  bj-sbceqgALT  32737  lsatcv0eq  33031  cmtbr2N  33237  atlatmstc  33303  1cvrco  33455  cdleme3  34220  cdleme7  34232  cdlemg10c  34622  dvhopellsm  35101  dibord  35143  dib1dim2  35152  diblsmopel  35155  dihopelvalcpre  35232  dih1dimatlem  35313  hdmap14lem13  35867  hdmapoc  35918