Theorem 3bitrd 307

Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)

Hypotheses

Ref	Expression
3bitrd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitrd.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))
3bitrd.3	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3bitrd	⊢ (𝜑 → (𝜓 ↔ 𝜏))

Proof of Theorem 3bitrd

Step	Hyp	Ref	Expression
1		3bitrd.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3bitrd.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	1, 2	bitrd 281	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 281	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  sbceqal  3835  2reu4lem  4465  elimhyp3v  4532  elimhyp4v  4533  keephyp3v  4538  opeqsng  5393  snopeqop  5396  frsn  5639  elpredg  6162  f1eq123d  6608  foeq123d  6609  f1oeq123d  6610  fnmptfvd  6811  fnotovb  7206  ofrfval  7417  eloprabi  7761  fnmpoovd  7782  suppsnop  7844  smoeq  7987  mapsnend  8588  infglbb  8955  wemapwe  9160  fseqenlem1  9450  dfac12lem2  9570  fin23lem22  9749  pwfseqlem5  10085  pwfseq  10086  enqbreq2  10342  lterpq  10392  ltdiv23  11531  lediv23  11532  negfi  11589  halfpos  11868  addltmul  11874  div4p1lem1div2  11893  supminf  12336  supxrbnd1  12715  supxrbnd2  12716  iccf1o  12883  fzshftral  12996  fzoshftral  13155  2tnp1ge0ge0  13200  dfceil2  13210  modirr  13311  hashen1  13732  seqcoll  13823  hash2prb  13831  hashle2prv  13837  s111  13969  swrdspsleq  14027  pfxnd0  14050  pfxeq  14058  wrd2ind  14085  2swrd2eqwrdeq  14315  eqwrds3  14325  limsupgle  14834  tanaddlem  15519  dvdssub  15654  addmodlteqALT  15675  dvdsmod  15678  oddp1even  15693  nn0o1gt2  15732  nn0oddm1d2  15736  bitscmp  15787  saddisjlem  15813  smueqlem  15839  ncoprmgcdne1b  15994  cncongr1  16011  cncongr2  16012  prmreclem5  16256  4sqlem11  16291  4sqlem17  16297  vdwmc2  16315  ismre  16861  acsfn  16930  dfiso2  17042  brcic  17068  isssc  17090  setcinv  17350  intopsn  17864  sgrp1  17910  sgrp2nmndlem4  18093  nmzsubg  18317  conjnmzb  18393  gsmsymgreqlem2  18559  symgfixels  18562  f1omvdconj  18574  oddvdsnn0  18672  oddvds  18675  odcong  18677  odf1  18689  dpjeq  19181  pgpfac1lem2  19197  ring1  19352  lsmspsn  19856  lbsacsbs  19928  lpigen  20029  prmirredlem  20640  znf1o  20698  znleval  20701  znunit  20710  islinds2  20957  islindf4  20982  scmatf1  21140  isclo  21695  maxlp  21755  1stccn  22071  xkoinjcn  22295  elmptrab  22435  fbunfip  22477  elfm  22555  fmid  22568  flfnei  22599  isflf  22601  isfcls  22617  fclsopn  22622  isfcf  22642  cnextfun  22672  eltsms  22741  prdsxmetlem  22978  elmopn  23052  metss  23118  comet  23123  elbl4  23173  metuel2  23175  nrmmetd  23184  metdsge  23457  tcphcph  23840  fmcfil  23875  cmscsscms  23976  rrxmet  24011  minveclem4  24035  shft2rab  24109  sca2rab  24113  volsup2  24206  mbfsup  24265  i1fmullem  24295  mbfi1fseqlem4  24319  xrge0f  24332  itg2monolem1  24351  ellimc2  24475  cnlimc  24486  mdegleb  24658  facth1  24758  ulm2  24973  sineq0  25109  coseq1  25110  efeq1  25113  sinord  25118  root1eq1  25336  angrtmuld  25386  affineequiv3  25403  quad2  25417  dcubic  25424  cubic2  25426  dquartlem1  25429  dquart  25431  quart  25439  rlimcnp  25543  lgamucov  25615  mumullem2  25757  chtub  25788  fsumvma  25789  fsumvma2  25790  chpchtsum  25795  dchrelbas2  25813  bposlem7  25866  lgsneg  25897  lgsne0  25911  lgsprme0  25915  lgsqrlem2  25923  lgsquadlem1  25956  lgsquadlem2  25957  2lgs  25983  2lgsoddprm  25992  2sqreultb  26035  istrkg3ld  26247  tgcgr4  26317  iscgra1  26596  isleag  26633  iseqlg  26653  axcontlem7  26756  elntg2  26771  edg0iedg0  26840  ausgrusgrb  26950  usgr1v0edg  27039  nb3grprlem2  27163  uvtx01vtx  27179  cplgr3v  27217  vtxd0nedgb  27270  vtxdusgr0edgnelALT  27278  1egrvtxdg0  27293  upgr2wlk  27450  wlkp1lem8  27462  wwlksnextbi  27672  s3wwlks2on  27735  elwwlks2  27745  elwspths2spth  27746  rusgrnumwwlkl1  27747  clwwlkwwlksb  27833  0pth  27904  upgriseupth  27986  eupth2lem2  27998  eupth2lem3lem4  28010  eupth2lem3lem6  28012  nfrgr2v  28051  frgr3v  28054  fusgr2wsp2nb  28113  fusgreg2wsp  28115  extwwlkfab  28131  numclwwlk2lem1  28155  frgrreggt1  28172  imsmetlem  28467  ipz  28496  bnsscmcl  28645  minvecolem4  28657  hvsubcan  28851  hoeq2  29608  leoptri  29913  atcv0eq  30156  elimifd  30298  gtiso  30436  2ndpreima  30443  fpwrelmapffslem  30468  xnn01gt  30495  fzsplit3  30517  isomnd  30702  ogrpinvlt  30724  islinds5  30932  smatrcl  31061  pstmfval  31136  lmlim  31190  dya2ub  31528  eulerpartlemr  31632  isrrvv  31701  ballotlemsima  31773  signsvfn  31852  subfacp1lem3  32429  subfacp1lem5  32431  erdszelem1  32438  erdsze  32449  erdsze2lem2  32451  satf0op  32624  fmlafvel  32632  isfmlasuc  32635  filnetlem4  33729  bj-issetwt  34192  bj-sbceqgALT  34222  bj-raldifsn  34395  bj-idreseq  34457  bj-elid6  34465  bj-imdirval3  34477  csbwrecsg  34611  poimirlem24  34931  itg2addnclem2  34959  ftc1anclem1  34982  areacirclem1  34997  areacirclem5  35001  metf1o  35045  isass  35139  rngosn3  35217  brxrn  35641  lsatcv0eq  36198  cmtbr2N  36404  atlatmstc  36470  1cvrco  36623  cdleme3  37388  cdleme7  37400  cdlemg10c  37790  dvhopellsm  38268  dibord  38310  dib1dim2  38319  diblsmopel  38322  dihopelvalcpre  38399  dih1dimatlem  38480  hdmap14lem13  39031  hdmapoc  39082  elrfirn  39312  jm2.19lem2  39607  pwfi2f1o  39716  proot1ex  39821  brfvidRP  40053  uneqsn  40393  ntrclsfveq  40432  ntrclskb  40439  ntrclsk3  40440  ntrneiel2  40456  k0004lem3  40519  bcc0  40692  pwpwuni  41339  disjinfi  41474  rnmptbd2  41541  rnmptbd  41548  infxrbnd2  41657  ltmulneg  41684  ltdiv23neg  41686  rexabsle  41713  uzub  41725  supxrleubrnmptf  41747  supminfxr  41760  limsupre2lem  42025  limsupre2mpt  42031  limsupre3mpt  42035  limsupreuz  42038  limsuplt2  42054  liminflimsupclim  42108  xlimpnfxnegmnf  42115  liminfpnfuz  42117  xlimclim  42125  xlimbr  42128  xlimclim2lem  42140  xlimmnfmpt  42144  xlimpnfmpt  42145  fourierdlem113  42524  isvonmbl  42940  reuf1odnf  43326  addsubeq0  43516  ltnltne  43519  iccpartgtl  43606  iccpartleu  43608  iccpartgel  43609  reuprpr  43705  fmtnoprmfac1  43747  fmtnoprmfac2  43749  quad1  43805  requad1  43807  requad2  43808  bits0ALTV  43864  bgoldbtbndlem1  43990  0nodd  44097  2nodd  44099  rngcinv  44272  rngcinvALTV  44284  ringcinv  44323  ringcinvALTV  44347  islindeps  44528  snlindsntor  44546  blen1b  44668  nn0sumshdiglem1  44701  rrx2plordisom  44730  ehl2eudis0lt  44733  eenglngeehlnmlem2  44745  rrx2linest  44749  line2  44759  line2x  44761  line2y  44762  itschlc0xyqsol1  44773  itsclquadeu  44784