Theorem 3bitrd 308

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 282	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 282	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  2reu4lem  4482  elimhyp3v  4553  elimhyp4v  4554  keephyp3v  4559  ralsng  4636  opeqsng  5480  snopeqop  5483  frsn  5745  f1eq123d  6844  foeq123d  6845  f1oeq123d  6846  fnmptfvd  7069  fnotovb  7501  ofrfvalg  7731  eloprabi  8107  fnmpoovd  8131  suppsnop  8231  smoeq  8394  naddasslem1  8740  naddasslem2  8741  mapsnend  9100  infglbb  9519  wemapwe  9733  fseqenlem1  10140  dfac12lem2  10260  fin23lem22  10442  pwfseqlem5  10785  pwfseq  10786  enqbreq2  11042  lterpq  11092  ltdiv23  12246  lediv23  12247  negfi  12304  halfpos  12614  addltmul  12620  div4p1lem1div2  12639  supminf  13100  supxrbnd1  13489  supxrbnd2  13490  iccf1o  13665  fzshftral  13787  fzoshftral  13960  2tnp1ge0ge0  14007  dfceil2  14017  modirr  14123  hashen1  14553  seqcoll  14648  hash2prb  14656  hashle2prv  14662  hash3tpb  14679  s111  14803  swrdspsleq  14855  pfxnd0  14878  pfxeq  14885  wrd2ind  14912  2swrd2eqwrdeq  15147  eqwrds3  15155  limsupgle  15685  tanaddlem  16375  difmod0  16498  dvdssub  16515  addmodlteqALT  16536  dvdsmod  16540  oddp1even  16555  nn0o1gt2  16592  nn0oddm1d2  16596  bitscmp  16649  saddisjlem  16675  smueqlem  16701  ncoprmgcdne1b  16866  cncongr1  16883  cncongr2  16884  prmreclem5  17139  4sqlem11  17174  4sqlem17  17180  vdwmc2  17198  ismre  17801  acsfn  17874  dfiso2  17988  brcic  18014  isssc  18036  setcinv  18306  cat1  18313  intopsn  18873  sgrp1  18959  sgrppropd  18961  sgrp2nmndlem4  19168  nmzsubg  19416  eqg0subg  19452  conjnmzb  19508  gsmsymgreqlem2  19687  symgfixels  19690  f1omvdconj  19702  oddvdsnn0  19800  oddvds  19803  odcong  19805  odf1  19818  dpjeq  20317  pgpfac1lem2  20333  isomnd  20379  ogrpinvlt  20400  ring1  20583  rngcinv  20931  ringcinv  20965  lsmspsn  21401  lbsacsbs  21476  rngqiprngimf1lem  21632  lpigen  21701  prmirredlem  21822  znf1o  21901  znleval  21904  znunit  21913  islinds2  22163  islindf4  22188  psdmul  22531  scmatf1  22890  isclo  23449  maxlp  23509  1stccn  23826  xkoinjcn  24050  elmptrab  24190  fbunfip  24232  elfm  24310  fmid  24323  flfnei  24354  isflf  24356  isfcls  24372  fclsopn  24377  isfcf  24397  cnextfun  24427  eltsms  24496  prdsxmetlem  24731  elmopn  24805  metss  24871  comet  24876  elbl4  24926  metuel2  24928  nrmmetd  24937  metdsge  25213  tcphcph  25602  fmcfil  25637  cmscsscms  25738  rrxmet  25773  minveclem4  25797  shft2rab  25873  sca2rab  25877  volsup2  25970  mbfsup  26029  i1fmullem  26059  mbfi1fseqlem4  26083  xrge0f  26096  itg2monolem1  26115  ellimc2  26241  cnlimc  26252  mdegleb  26426  r1pid2  26524  facth1  26529  rnplynfin  26674  ulm2  26758  sineq0  26898  coseq1  26899  efeq1  26902  sinord  26908  root1eq1  27129  angrtmuld  27182  affineequiv3  27199  quad2  27213  dcubic  27220  cubic2  27222  dquartlem1  27225  dquart  27227  quart  27235  rlimcnp  27339  lgamucov  27411  mumullem2  27553  chtub  27585  fsumvma  27586  fsumvma2  27587  chpchtsum  27592  dchrelbas2  27610  bposlem7  27663  lgsneg  27694  lgsne0  27708  lgsprme0  27712  lgsqrlem2  27720  lgsquadlem1  27753  lgsquadlem2  27754  2lgs  27780  2lgsoddprm  27789  2sqreultb  27832  fltoprmgt3  28042  lrrecval2  28372  subscan1d  28535  n0lesm1lt  28799  bdaypw2bnd  28897  elreno2  28927  istrkg3ld  28969  tgcgr4  29040  iscgra1  29363  isleag  29412  iseqlg  29458  axcontlem7  29594  elntg2  29609  edg0iedg0  29679  ausgrusgrb  29792  usgr1v0edg  29884  nb3grprlem2  30008  uvtx01vtx  30024  cplgr3v  30062  vtxd0nedgb  30115  vtxdusgr0edgnelALT  30123  1egrvtxdg0  30138  upgr2wlk  30293  wlkp1lem8  30305  dfpth2  30360  wwlksnextbi  30529  s3wwlks2on  30591  sps3wwlks2on  30592  elwwlks2  30604  elwspths2spth  30605  rusgrnumwwlkl1  30606  clwwlkwwlksb  30691  0pth  30762  upgriseupth  30854  eupth2lem2  30866  eupth2lem3lem4  30878  eupth2lem3lem6  30880  nfrgr2v  30919  frgr3v  30922  fusgr2wsp2nb  30981  fusgreg2wsp  30983  extwwlkfab  30999  numclwwlk2lem1  31023  frgrreggt1  31040  imsmetlem  31338  ipz  31367  bnsscmcl  31516  minvecolem4  31528  hvsubcan  31722  hoeq2  32479  leoptri  32784  atcv0eq  33027  elimifd  33227  fdifsupp  33365  ressupprn  33370  gtiso  33381  2ndpreima  33388  fpwrelmapffslem  33410  quad3d  33427  xnn01gt  33448  fzsplit3  33471  fzo0opth  33481  rlocisunit  33926  islinds5  34020  grplsmid  34052  selvply1rhmlem2  34257  fldextrspunlsp  34410  constrsuc  34474  smatrcl  34532  rhmpreimacnlem  34620  pstmfval  34632  lmlim  34683  dya2ub  35006  eulerpartlemr  35110  isrrvv  35179  ballotlemsima  35252  signsvfn  35315  maxssj0  36040  subfacp1lem3  36148  subfacp1lem5  36150  erdszelem1  36157  erdsze  36168  erdsze2lem2  36170  satf0op  36343  fmlafvel  36351  isfmlasuc  36354  filnetlem4  37377  bj-issetwt  37995  bj-sbceqgALT  38022  bj-raldifsn  38284  bj-idreseq  38344  bj-elid6  38352  bj-imdirval3  38366  bj-imdirco  38372  poimirlem24  38823  itg2addnclem2  38851  ftc1anclem1  38872  areacirclem1  38887  areacirclem5  38891  metf1o  38948  isass  39039  rngosn3  39117  brxrn  39574  lsatcv0eq  40363  cmtbr2N  40569  atlatmstc  40635  1cvrco  40788  cdleme3  41553  cdleme7  41565  cdlemg10c  41955  dvhopellsm  42433  dibord  42475  dib1dim2  42484  diblsmopel  42487  dihopelvalcpre  42564  dih1dimatlem  42645  hdmap14lem13  43196  hdmapoc  43247  quadfac  43514  cxp112d  43652  cxp111d  43653  elrfirn  43966  jm2.19lem2  44257  pwfi2f1o  44358  proot1ex  44453  isoeq145d  44675  sqrtcval  44896  brfvidRP  44943  uneqsn  45280  ntrclsfveq  45317  ntrclskb  45324  ntrclsk3  45325  ntrneiel2  45341  k0004lem3  45404  bcc0  45579  pwpwuni  46342  disjinfi  46474  rnmptbd2  46528  rnmptbd  46535  infxrbnd2  46647  ltmulneg  46670  ltdiv23neg  46672  rexabsle  46696  uzub  46708  supxrleubrnmptf  46728  supminfxr  46741  limsupre2lem  47001  limsupre2mpt  47007  limsupre3mpt  47011  limsupreuz  47014  limsuplt2  47030  liminflimsupclim  47084  xlimpnfxnegmnf  47091  liminfpnfuz  47093  xlimclim  47101  xlimbr  47104  xlimclim2lem  47116  xlimmnfmpt  47120  xlimpnfmpt  47121  fourierdlem113  47496  isvonmbl  47915  chnsubseqwl  48156  reuf1odnf  48445  addsubeq0  48633  ltnltne  48636  ceilbi  48674  iccpartgtl  48775  iccpartleu  48777  iccpartgel  48778  reuprpr  48872  fmtnoprmfac1  48917  fmtnoprmfac2  48919  quad1  48985  requad1  48987  requad2  48988  bits0ALTV  49044  bgoldbtbndlem1  49170  clnbgrel  49193  clnbupgrel  49199  dfsclnbgr6  49223  isubgredg  49231  gpgiedgdmel  49414  opgpgvtx  49420  gpg3kgrtriexlem5  49452  0nodd  49534  2nodd  49536  rngcinvALTV  49640  ringcinvALTV  49674  crngprmringidom  49763  islindeps  49890  snlindsntor  49908  blen1b  50025  nn0sumshdiglem1  50058  0aryfvalel  50071  rrx2plordisom  50161  ehl2eudis0lt  50164  eenglngeehlnmlem2  50176  rrx2linest  50179  line2  50189  line2x  50191  line2y  50192  itschlc0xyqsol1  50203  itsclquadeu  50214  itscnhlinecirc02p  50222  map0cor  50291  joindm2  50407  meetdm2  50409  islmd  51173  iscmd  51174