Theorem 3bitrd 305

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  2reu4lem  4495  elimhyp3v  4566  elimhyp4v  4567  keephyp3v  4572  ralsng  4649  opeqsng  5476  snopeqop  5479  frsn  5740  f1eq123d  6807  foeq123d  6808  f1oeq123d  6809  fnmptfvd  7028  fnotovb  7452  ofrfvalg  7674  eloprabi  8057  fnmpoovd  8081  suppsnop  8172  smoeq  8359  naddasslem1  8701  naddasslem2  8702  mapsnend  9045  infglbb  9498  wemapwe  9704  fseqenlem1  10031  dfac12lem2  10152  fin23lem22  10334  pwfseqlem5  10670  pwfseq  10671  enqbreq2  10927  lterpq  10977  ltdiv23  12126  lediv23  12127  negfi  12184  halfpos  12464  addltmul  12470  div4p1lem1div2  12489  supminf  12944  supxrbnd1  13330  supxrbnd2  13331  iccf1o  13503  fzshftral  13622  fzoshftral  13790  2tnp1ge0ge0  13836  dfceil2  13846  modirr  13950  hashen1  14378  seqcoll  14472  hash2prb  14480  hashle2prv  14486  hash3tpb  14503  s111  14622  swrdspsleq  14672  pfxnd0  14695  pfxeq  14703  wrd2ind  14730  2swrd2eqwrdeq  14961  eqwrds3  14969  limsupgle  15482  tanaddlem  16171  dvdssub  16310  addmodlteqALT  16331  dvdsmod  16335  oddp1even  16350  nn0o1gt2  16387  nn0oddm1d2  16391  bitscmp  16444  saddisjlem  16470  smueqlem  16496  ncoprmgcdne1b  16656  cncongr1  16673  cncongr2  16674  prmreclem5  16927  4sqlem11  16962  4sqlem17  16968  vdwmc2  16986  ismre  17589  acsfn  17658  dfiso2  17772  brcic  17798  isssc  17820  setcinv  18090  cat1  18097  intopsn  18619  sgrp1  18694  sgrppropd  18696  sgrp2nmndlem4  18893  nmzsubg  19135  eqg0subg  19166  conjnmzb  19223  gsmsymgreqlem2  19399  symgfixels  19402  f1omvdconj  19414  oddvdsnn0  19512  oddvds  19515  odcong  19517  odf1  19530  dpjeq  20029  pgpfac1lem2  20045  ring1  20257  rngcinv  20584  ringcinv  20618  lsmspsn  21029  lbsacsbs  21104  rngqiprngimf1lem  21242  lpigen  21283  prmirredlem  21420  znf1o  21499  znleval  21502  znunit  21511  islinds2  21760  islindf4  21785  psdmul  22091  scmatf1  22456  isclo  23012  maxlp  23072  1stccn  23388  xkoinjcn  23612  elmptrab  23752  fbunfip  23794  elfm  23872  fmid  23885  flfnei  23916  isflf  23918  isfcls  23934  fclsopn  23939  isfcf  23959  cnextfun  23989  eltsms  24058  prdsxmetlem  24294  elmopn  24368  metss  24434  comet  24439  elbl4  24489  metuel2  24491  nrmmetd  24500  metdsge  24776  tcphcph  25176  fmcfil  25211  cmscsscms  25312  rrxmet  25347  minveclem4  25371  shft2rab  25448  sca2rab  25452  volsup2  25545  mbfsup  25604  i1fmullem  25634  mbfi1fseqlem4  25658  xrge0f  25671  itg2monolem1  25690  ellimc2  25817  cnlimc  25828  mdegleb  26008  r1pid2  26106  facth1  26111  ulm2  26333  sineq0  26471  coseq1  26472  efeq1  26475  sinord  26481  root1eq1  26703  angrtmuld  26756  affineequiv3  26773  quad2  26787  dcubic  26794  cubic2  26796  dquartlem1  26799  dquart  26801  quart  26809  rlimcnp  26913  lgamucov  26986  mumullem2  27128  chtub  27161  fsumvma  27162  fsumvma2  27163  chpchtsum  27168  dchrelbas2  27186  bposlem7  27239  lgsneg  27270  lgsne0  27284  lgsprme0  27288  lgsqrlem2  27296  lgsquadlem1  27329  lgsquadlem2  27330  2lgs  27356  2lgsoddprm  27365  2sqreultb  27408  lrrecval2  27878  istrkg3ld  28374  tgcgr4  28444  iscgra1  28723  isleag  28760  iseqlg  28780  axcontlem7  28883  elntg2  28898  edg0iedg0  28968  ausgrusgrb  29078  usgr1v0edg  29170  nb3grprlem2  29294  uvtx01vtx  29310  cplgr3v  29348  vtxd0nedgb  29402  vtxdusgr0edgnelALT  29410  1egrvtxdg0  29425  upgr2wlk  29582  wlkp1lem8  29594  dfpth2  29645  wwlksnextbi  29810  s3wwlks2on  29872  elwwlks2  29882  elwspths2spth  29883  rusgrnumwwlkl1  29884  clwwlkwwlksb  29969  0pth  30040  upgriseupth  30122  eupth2lem2  30134  eupth2lem3lem4  30146  eupth2lem3lem6  30148  nfrgr2v  30187  frgr3v  30190  fusgr2wsp2nb  30249  fusgreg2wsp  30251  extwwlkfab  30267  numclwwlk2lem1  30291  frgrreggt1  30308  imsmetlem  30605  ipz  30634  bnsscmcl  30783  minvecolem4  30795  hvsubcan  30989  hoeq2  31746  leoptri  32051  atcv0eq  32294  elimifd  32458  fdifsupp  32596  ressupprn  32601  gtiso  32612  2ndpreima  32619  fpwrelmapffslem  32645  quad3d  32663  xnn01gt  32684  fzsplit3  32707  fzo0opth  32719  isomnd  33006  ogrpinvlt  33028  islinds5  33319  grplsmid  33356  r1pid2OLD  33553  fldextrspunlsp  33650  constrsuc  33707  smatrcl  33756  rhmpreimacnlem  33844  pstmfval  33856  lmlim  33907  dya2ub  34231  eulerpartlemr  34335  isrrvv  34404  ballotlemsima  34477  signsvfn  34543  subfacp1lem3  35133  subfacp1lem5  35135  erdszelem1  35142  erdsze  35153  erdsze2lem2  35155  satf0op  35328  fmlafvel  35336  isfmlasuc  35339  filnetlem4  36328  bj-issetwt  36822  bj-sbceqgALT  36849  bj-raldifsn  37047  bj-idreseq  37109  bj-elid6  37117  bj-imdirval3  37131  bj-imdirco  37137  poimirlem24  37597  itg2addnclem2  37625  ftc1anclem1  37646  areacirclem1  37661  areacirclem5  37665  metf1o  37708  isass  37799  rngosn3  37877  brxrn  38321  lsatcv0eq  38994  cmtbr2N  39200  atlatmstc  39266  1cvrco  39420  cdleme3  40185  cdleme7  40197  cdlemg10c  40587  dvhopellsm  41065  dibord  41107  dib1dim2  41116  diblsmopel  41119  dihopelvalcpre  41196  dih1dimatlem  41277  hdmap14lem13  41828  hdmapoc  41879  cxp112d  42322  cxp111d  42323  elrfirn  42650  jm2.19lem2  42946  pwfi2f1o  43052  proot1ex  43152  isoeq145d  43375  sqrtcval  43597  brfvidRP  43644  uneqsn  43981  ntrclsfveq  44018  ntrclskb  44025  ntrclsk3  44026  ntrneiel2  44042  k0004lem3  44105  bcc0  44297  pwpwuni  45015  disjinfi  45150  rnmptbd2  45207  rnmptbd  45214  infxrbnd2  45330  ltmulneg  45353  ltdiv23neg  45355  rexabsle  45380  uzub  45392  supxrleubrnmptf  45412  supminfxr  45425  limsupre2lem  45689  limsupre2mpt  45695  limsupre3mpt  45699  limsupreuz  45702  limsuplt2  45718  liminflimsupclim  45772  xlimpnfxnegmnf  45779  liminfpnfuz  45781  xlimclim  45789  xlimbr  45792  xlimclim2lem  45804  xlimmnfmpt  45808  xlimpnfmpt  45809  fourierdlem113  46184  isvonmbl  46603  reuf1odnf  47072  addsubeq0  47261  ltnltne  47264  iccpartgtl  47366  iccpartleu  47368  iccpartgel  47369  reuprpr  47463  fmtnoprmfac1  47505  fmtnoprmfac2  47507  quad1  47560  requad1  47562  requad2  47563  bits0ALTV  47619  bgoldbtbndlem1  47745  clnbgrel  47768  clnbupgrel  47774  dfsclnbgr6  47797  isubgredg  47805  opgpgvtx  47963  gpg3kgrtriexlem5  47996  0nodd  48039  2nodd  48041  rngcinvALTV  48145  ringcinvALTV  48179  islindeps  48323  snlindsntor  48341  blen1b  48462  nn0sumshdiglem1  48495  0aryfvalel  48508  rrx2plordisom  48597  ehl2eudis0lt  48600  eenglngeehlnmlem2  48612  rrx2linest  48616  line2  48626  line2x  48628  line2y  48629  itschlc0xyqsol1  48640  itsclquadeu  48651  map0cor  48727  joindm2  48836  meetdm2  48838