Theorem 3bitrd 294

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

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

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 197

This theorem is referenced by:  sbceqal  3487  elimhyp3v  4148  elimhyp4v  4149  keephyp3v  4154  frsn  5189  elpredg  5694  f1eq123d  6131  foeq123d  6132  f1oeq123d  6133  fnmptfvd  6320  ofrfval  6905  eloprabi  7232  fnmpt2ovd  7252  suppsnop  7309  smoeq  7447  infglbb  8397  wemapwe  8594  fseqenlem1  8847  dfac12lem2  8966  fin23lem22  9149  pwfseqlem5  9485  pwfseq  9486  enqbreq2  9742  lterpq  9792  ltdiv23  10914  lediv23  10915  negfi  10971  halfpos  11262  addltmul  11268  div4p1lem1div2  11287  supminf  11775  supxrbnd1  12151  supxrbnd2  12152  iccf1o  12316  fzshftral  12428  fzoshftral  12585  2tnp1ge0ge0  12630  dfceil2  12640  modirr  12741  hashen1  13160  seqcoll  13248  hash2prb  13254  hashle2prv  13260  s111  13395  swrdeq  13444  wrd2ind  13477  2swrd2eqwrdeq  13696  eqwrds3  13704  limsupgle  14208  tanaddlem  14896  dvdssub  15026  addmodlteqALT  15047  dvdsmod  15050  oddp1even  15068  nn0o1gt2  15097  nn0oddm1d2  15101  bitscmp  15160  saddisjlem  15186  smueqlem  15212  ncoprmgcdne1b  15363  cncongr1  15381  cncongr2  15382  prmreclem5  15624  4sqlem11  15659  4sqlem17  15665  vdwmc2  15683  ismre  16250  acsfn  16320  dfiso2  16432  brcic  16458  isssc  16480  setcinv  16740  intopsn  17253  sgrp1  17293  sgrp2nmndlem4  17415  nmzsubg  17635  conjnmzb  17695  gsmsymgreqlem2  17851  symgfixels  17854  f1omvdconj  17866  oddvdsnn0  17963  oddvds  17966  odcong  17968  odf1  17979  dpjeq  18458  pgpfac1lem2  18474  ring1  18602  lsmspsn  19084  lbsacsbs  19156  lpigen  19256  prmirredlem  19841  znf1o  19900  znleval  19903  znunit  19912  islinds2  20152  islindf4  20177  scmatf1  20337  isclo  20891  maxlp  20951  1stccn  21266  xkoinjcn  21490  elmptrab  21630  fbunfip  21673  elfm  21751  fmid  21764  flfnei  21795  isflf  21797  isfcls  21813  fclsopn  21818  isfcf  21838  cnextfun  21868  eltsms  21936  prdsxmetlem  22173  elmopn  22247  metss  22313  comet  22318  elbl4  22368  metuel2  22370  nrmmetd  22379  metdsge  22652  tchcph  23036  fmcfil  23070  rrxmet  23191  minveclem4  23203  shft2rab  23276  sca2rab  23280  volsup2  23373  mbfsup  23431  i1fmullem  23461  mbfi1fseqlem4  23485  xrge0f  23498  itg2monolem1  23517  ellimc2  23641  cnlimc  23652  mdegleb  23824  facth1  23924  ulm2  24139  sineq0  24273  coseq1  24274  efeq1  24275  sinord  24280  root1eq1  24496  angrtmuld  24538  quad2  24566  dcubic  24573  cubic2  24575  dquartlem1  24578  dquart  24580  quart  24588  rlimcnp  24692  lgamucov  24764  mumullem2  24906  chtub  24937  fsumvma  24938  fsumvma2  24939  chpchtsum  24944  bposlem7  25015  lgsneg  25046  lgsne0  25060  lgsprme0  25064  lgsqrlem2  25072  lgsquadlem1  25105  lgsquadlem2  25106  2lgs  25132  2lgsoddprm  25141  istrkg3ld  25360  tgcgr4  25426  iscgra1  25702  isleag  25733  iseqlg  25747  axcontlem7  25850  edg0iedg0  25949  edg0iedg0OLD  25950  ausgrusgrb  26060  usgr1v0edg  26149  nb3grprlem2  26283  uvtxa01vtx0  26297  cplgr3v  26331  vtxd0nedgb  26384  vtxdusgr0edgnelALT  26392  1egrvtxdg0  26407  wlkeq  26529  upgr2wlk  26564  wlkp1lem8  26577  wwlksnextbi  26789  wspthsnwspthsnon  26811  s3wwlks2on  26849  elwwlks2  26861  elwspths2spth  26862  rusgrnumwwlkl1  26863  0pth  26986  upgriseupth  27067  eupth2lem2  27079  eupth2lem3lem4  27091  eupth2lem3lem6  27093  nfrgr2v  27136  frgr3v  27139  fusgr2wsp2nb  27198  fusgreg2wsp  27200  extwwlkfab  27223  numclwwlk2lem1  27235  frgrreggt1  27251  imsmetlem  27545  ipz  27574  bnsscmcl  27724  minvecolem4  27736  hvsubcan  27931  hoeq2  28690  leoptri  28995  atcv0eq  29238  elimifd  29362  gtiso  29478  2ndpreima  29485  fpwrelmapffslem  29507  fzsplit3  29553  isomnd  29701  ogrpinvlt  29724  smatrcl  29862  pstmfval  29939  lmlim  29993  dya2ub  30332  eulerpartlemr  30436  isrrvv  30505  ballotlemsima  30577  signsvfn  30659  subfacp1lem3  31164  subfacp1lem5  31166  erdszelem1  31173  erdsze  31184  erdsze2lem2  31186  filnetlem4  32376  bj-issetwt  32859  bj-sbceqgALT  32897  bj-raldifsn  33054  csbwrecsg  33173  poimirlem24  33433  itg2addnclem2  33462  ftc1anclem1  33485  areacirclem1  33500  areacirclem5  33504  metf1o  33551  isass  33645  rngosn3  33723  lsatcv0eq  34334  cmtbr2N  34540  atlatmstc  34606  1cvrco  34758  cdleme3  35524  cdleme7  35536  cdlemg10c  35927  dvhopellsm  36406  dibord  36448  dib1dim2  36457  diblsmopel  36460  dihopelvalcpre  36537  dih1dimatlem  36618  hdmap14lem13  37172  hdmapoc  37223  elrfirn  37258  jm2.19lem2  37557  pwfi2f1o  37666  proot1ex  37779  brfvidRP  37980  uneqsn  38321  ntrclsfveq  38360  ntrclskb  38367  ntrclsk3  38368  ntrneiel2  38384  k0004lem3  38447  bcc0  38539  pwpwuni  39225  rnmptpr  39358  disjinfi  39380  mapsnend  39391  rnmptbd2  39464  rnmptbd  39471  infxrbnd2  39585  ltmulneg  39615  ltdiv23neg  39617  rexabsle  39646  uzub  39658  supxrleubrnmptf  39680  supminfxr  39694  limsupre2lem  39956  limsupre2mpt  39962  limsupre3mpt  39966  limsupreuz  39969  limsuplt2  39985  liminflimsupclim  40039  xlimclim  40050  xlimbr  40053  xlimclim2lem  40065  xlimmnfmpt  40069  xlimpnfmpt  40070  fourierdlem113  40436  isvonmbl  40852  2reu4a  41189  ltnltne  41313  iccpartgtl  41362  iccpartleu  41364  iccpartgel  41365  pfxeq  41404  fmtnoprmfac1  41477  fmtnoprmfac2  41479  bits0ALTV  41590  bgoldbtbndlem1  41693  0nodd  41810  2nodd  41812  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056  islindeps  42242  snlindsntor  42260  blen1b  42382  nn0sumshdiglem1  42415