Theorem 3bitrd 271

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

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

This theorem is referenced by:  sbceqal  3172  sbcnel12g  3228  elimhyp3v  3749  elimhyp4v  3750  keephyp3v  3755  f1eq123d  5628  foeq123d  5629  f1oeq123d  5630  ofrfval  6272  eloprabi  6372  smoeq  6571  wemapwe  7610  fseqenlem1  7861  dfac12lem2  7980  fin23lem22  8163  pwfseqlem5  8494  pwfseq  8495  enqbreq2  8753  lterpq  8803  ltdiv23  9857  lediv23  9858  halfpos  10154  addltmul  10159  supminf  10519  supxrbnd1  10856  supxrbnd2  10857  iccf1o  10995  fzshftral  11089  modirr  11241  seqcoll  11667  s111  11717  limsupgle  12226  tanaddlem  12722  dvdssub  12845  dvdsmod  12861  oddp1even  12865  bitscmp  12905  saddisjlem  12931  smueqlem  12957  prmreclem5  13243  4sqlem11  13278  4sqlem17  13284  vdwmc2  13302  ismre  13770  acsfn  13839  isssc  13975  setcinv  14200  nmzsubg  14936  conjnmzb  14995  oddvdsnn0  15137  oddvds  15140  odcong  15142  odf1  15153  dpjeq  15572  pgpfac1lem2  15588  lsmspsn  16111  lbsacsbs  16183  lpigen  16282  prmirredlem  16728  znf1o  16787  znunit  16799  isclo  17106  maxlp  17165  1stccn  17479  xkoinjcn  17672  elmptrab  17812  fbunfip  17854  elfm  17932  fmid  17945  flfnei  17976  isflf  17978  isfcls  17994  fclsopn  17999  isfcf  18019  cnextfun  18048  eltsms  18115  prdsxmetlem  18351  elmopn  18425  metss  18491  comet  18496  elbl4  18559  metuel2  18562  nrmmetd  18575  metdsge  18832  tchcph  19147  fmcfil  19178  minveclem4  19286  shft2rab  19357  sca2rab  19361  volsup2  19450  mbfsup  19509  i1fmullem  19539  mbfi1fseqlem4  19563  xrge0f  19576  itg2monolem1  19595  ellimc2  19717  cnlimc  19728  mdegleb  19940  facth1  20040  ulm2  20254  sineq0  20382  coseq1  20383  efeq1  20384  sinord  20389  root1eq1  20592  angrtmuld  20603  quad2  20632  dcubic  20639  cubic2  20641  dquartlem1  20644  dquart  20646  quart  20654  rlimcnp  20757  mumullem2  20916  chtub  20949  fsumvma  20950  fsumvma2  20951  chpchtsum  20956  bposlem7  21027  lgsneg  21056  lgsne0  21070  lgsqrlem2  21079  lgsquadlem1  21091  lgsquadlem2  21092  isuslgra  21325  isusgra  21326  ausisusgra  21333  nb3graprlem2  21414  cusgra3v  21426  sizeusglecusg  21448  uvtx01vtx  21454  is2wlk  21518  0pth  21523  wlkdvspthlem  21560  eupath2lem2  21653  eupath2lem3  21654  isass  21857  rngosn3  21967  imsmetlem  22135  ipz  22171  bnsscmcl  22323  minvecolem4  22335  hvsubcan  22529  hoeq2  23287  leoptri  23592  atcv0eq  23835  elimifd  23957  gtiso  24041  2ndpreima  24049  fzsplit3  24103  isofld  24188  pstmfval  24244  lmlim  24286  dya2ub  24573  isrrvv  24654  ballotlemsima  24726  lgamucov  24775  subfacp1lem3  24821  subfacp1lem5  24823  erdszelem1  24830  erdsze  24841  erdsze2lem2  24843  elpredg  25392  axcontlem7  25813  itg2addnclem2  26156  areacirclem2  26181  areacirclem3  26182  areacirclem6  26186  filnetlem4  26300  metf1o  26351  elrfirn  26639  jm2.19lem2  26951  islinds2  27151  islindf4  27176  f1omvdconj  27257  proot1ex  27388  2reu4a  27834  el2wlkonotot0  28069  el2wlkonotot  28070  el2wlksoton  28075  el2spthsoton  28076  el2wlksot  28077  el2pthsot  28078  frgra3v  28106  usg2spot2nb  28168  bnj1452  29127  lsatcv0eq  29530  cmtbr2N  29736  atlatmstc  29802  1cvrco  29954  cdleme3  30719  cdleme7  30731  cdlemg10c  31121  dvhopellsm  31600  dibord  31642  dib1dim2  31651  diblsmopel  31654  dihopelvalcpre  31731  dih1dimatlem  31812  hdmap14lem13  32366  hdmapoc  32417

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178