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  4473  elimhyp3v  4544  elimhyp4v  4545  keephyp3v  4550  ralsng  4629  opeqsng  5448  snopeqop  5451  frsn  5709  f1eq123d  6763  foeq123d  6764  f1oeq123d  6765  fnmptfvd  6983  fnotovb  7407  ofrfvalg  7627  eloprabi  8004  fnmpoovd  8026  suppsnop  8117  smoeq  8279  naddasslem1  8618  naddasslem2  8619  mapsnend  8969  infglbb  9387  wemapwe  9598  fseqenlem1  9926  dfac12lem2  10047  fin23lem22  10229  pwfseqlem5  10565  pwfseq  10566  enqbreq2  10822  lterpq  10872  ltdiv23  12024  lediv23  12025  negfi  12082  halfpos  12362  addltmul  12368  div4p1lem1div2  12387  supminf  12839  supxrbnd1  13227  supxrbnd2  13228  iccf1o  13403  fzshftral  13522  fzoshftral  13694  2tnp1ge0ge0  13740  dfceil2  13750  modirr  13856  hashen1  14284  seqcoll  14378  hash2prb  14386  hashle2prv  14392  hash3tpb  14409  s111  14530  swrdspsleq  14580  pfxnd0  14603  pfxeq  14610  wrd2ind  14637  2swrd2eqwrdeq  14867  eqwrds3  14875  limsupgle  15391  tanaddlem  16082  difmod0  16205  dvdssub  16222  addmodlteqALT  16243  dvdsmod  16247  oddp1even  16262  nn0o1gt2  16299  nn0oddm1d2  16303  bitscmp  16356  saddisjlem  16382  smueqlem  16408  ncoprmgcdne1b  16568  cncongr1  16585  cncongr2  16586  prmreclem5  16839  4sqlem11  16874  4sqlem17  16880  vdwmc2  16898  ismre  17500  acsfn  17573  dfiso2  17687  brcic  17713  isssc  17735  setcinv  18005  cat1  18012  intopsn  18570  sgrp1  18645  sgrppropd  18647  sgrp2nmndlem4  18844  nmzsubg  19085  eqg0subg  19116  conjnmzb  19173  gsmsymgreqlem2  19351  symgfixels  19354  f1omvdconj  19366  oddvdsnn0  19464  oddvds  19467  odcong  19469  odf1  19482  dpjeq  19981  pgpfac1lem2  19997  isomnd  20043  ogrpinvlt  20064  ring1  20236  rngcinv  20561  ringcinv  20595  lsmspsn  21027  lbsacsbs  21102  rngqiprngimf1lem  21240  lpigen  21281  prmirredlem  21418  znf1o  21497  znleval  21500  znunit  21509  islinds2  21759  islindf4  21784  psdmul  22100  scmatf1  22466  isclo  23022  maxlp  23082  1stccn  23398  xkoinjcn  23622  elmptrab  23762  fbunfip  23804  elfm  23882  fmid  23895  flfnei  23926  isflf  23928  isfcls  23944  fclsopn  23949  isfcf  23969  cnextfun  23999  eltsms  24068  prdsxmetlem  24303  elmopn  24377  metss  24443  comet  24448  elbl4  24498  metuel2  24500  nrmmetd  24509  metdsge  24785  tcphcph  25184  fmcfil  25219  cmscsscms  25320  rrxmet  25355  minveclem4  25379  shft2rab  25456  sca2rab  25460  volsup2  25553  mbfsup  25612  i1fmullem  25642  mbfi1fseqlem4  25666  xrge0f  25679  itg2monolem1  25698  ellimc2  25825  cnlimc  25836  mdegleb  26016  r1pid2  26114  facth1  26119  ulm2  26341  sineq0  26480  coseq1  26481  efeq1  26484  sinord  26490  root1eq1  26712  angrtmuld  26765  affineequiv3  26782  quad2  26796  dcubic  26803  cubic2  26805  dquartlem1  26808  dquart  26810  quart  26818  rlimcnp  26922  lgamucov  26995  mumullem2  27137  chtub  27170  fsumvma  27171  fsumvma2  27172  chpchtsum  27177  dchrelbas2  27195  bposlem7  27248  lgsneg  27279  lgsne0  27293  lgsprme0  27297  lgsqrlem2  27305  lgsquadlem1  27338  lgsquadlem2  27339  2lgs  27365  2lgsoddprm  27374  2sqreultb  27417  lrrecval2  27903  subscan1d  28062  n0slem1lt  28313  istrkg3ld  28459  tgcgr4  28529  iscgra1  28808  isleag  28845  iseqlg  28865  axcontlem7  28969  elntg2  28984  edg0iedg0  29054  ausgrusgrb  29164  usgr1v0edg  29256  nb3grprlem2  29380  uvtx01vtx  29396  cplgr3v  29434  vtxd0nedgb  29488  vtxdusgr0edgnelALT  29496  1egrvtxdg0  29511  upgr2wlk  29666  wlkp1lem8  29678  dfpth2  29728  wwlksnextbi  29893  s3wwlks2on  29955  sps3wwlks2on  29956  elwwlks2  29968  elwspths2spth  29969  rusgrnumwwlkl1  29970  clwwlkwwlksb  30055  0pth  30126  upgriseupth  30208  eupth2lem2  30220  eupth2lem3lem4  30232  eupth2lem3lem6  30234  nfrgr2v  30273  frgr3v  30276  fusgr2wsp2nb  30335  fusgreg2wsp  30337  extwwlkfab  30353  numclwwlk2lem1  30377  frgrreggt1  30394  imsmetlem  30691  ipz  30720  bnsscmcl  30869  minvecolem4  30881  hvsubcan  31075  hoeq2  31832  leoptri  32137  atcv0eq  32380  elimifd  32544  fdifsupp  32690  ressupprn  32695  gtiso  32706  2ndpreima  32713  fpwrelmapffslem  32739  quad3d  32757  xnn01gt  32778  fzsplit3  32801  fzo0opth  32811  islinds5  33376  grplsmid  33413  r1pid2OLD  33618  fldextrspunlsp  33759  constrsuc  33823  smatrcl  33881  rhmpreimacnlem  33969  pstmfval  33981  lmlim  34032  dya2ub  34355  eulerpartlemr  34459  isrrvv  34528  ballotlemsima  34601  signsvfn  34667  subfacp1lem3  35298  subfacp1lem5  35300  erdszelem1  35307  erdsze  35318  erdsze2lem2  35320  satf0op  35493  fmlafvel  35501  isfmlasuc  35504  filnetlem4  36497  bj-issetwt  36992  bj-sbceqgALT  37019  bj-raldifsn  37217  bj-idreseq  37279  bj-elid6  37287  bj-imdirval3  37301  bj-imdirco  37307  poimirlem24  37757  itg2addnclem2  37785  ftc1anclem1  37806  areacirclem1  37821  areacirclem5  37825  metf1o  37868  isass  37959  rngosn3  38037  brxrn  38480  lsatcv0eq  39219  cmtbr2N  39425  atlatmstc  39491  1cvrco  39644  cdleme3  40409  cdleme7  40421  cdlemg10c  40811  dvhopellsm  41289  dibord  41331  dib1dim2  41340  diblsmopel  41343  dihopelvalcpre  41420  dih1dimatlem  41501  hdmap14lem13  42052  hdmapoc  42103  cxp112d  42511  cxp111d  42512  elrfirn  42852  jm2.19lem2  43147  pwfi2f1o  43253  proot1ex  43353  isoeq145d  43576  sqrtcval  43798  brfvidRP  43845  uneqsn  44182  ntrclsfveq  44219  ntrclskb  44226  ntrclsk3  44227  ntrneiel2  44243  k0004lem3  44306  bcc0  44497  pwpwuni  45218  disjinfi  45352  rnmptbd2  45409  rnmptbd  45416  infxrbnd2  45529  ltmulneg  45552  ltdiv23neg  45554  rexabsle  45579  uzub  45591  supxrleubrnmptf  45611  supminfxr  45624  limsupre2lem  45884  limsupre2mpt  45890  limsupre3mpt  45894  limsupreuz  45897  limsuplt2  45913  liminflimsupclim  45967  xlimpnfxnegmnf  45974  liminfpnfuz  45976  xlimclim  45984  xlimbr  45987  xlimclim2lem  45999  xlimmnfmpt  46003  xlimpnfmpt  46004  fourierdlem113  46379  isvonmbl  46798  chnsubseqwl  47039  reuf1odnf  47269  addsubeq0  47458  ltnltne  47461  ceilbi  47495  iccpartgtl  47588  iccpartleu  47590  iccpartgel  47591  reuprpr  47685  fmtnoprmfac1  47727  fmtnoprmfac2  47729  quad1  47782  requad1  47784  requad2  47785  bits0ALTV  47841  bgoldbtbndlem1  47967  clnbgrel  47990  clnbupgrel  47996  dfsclnbgr6  48020  isubgredg  48028  gpgiedgdmel  48211  opgpgvtx  48217  gpg3kgrtriexlem5  48249  0nodd  48332  2nodd  48334  rngcinvALTV  48438  ringcinvALTV  48472  islindeps  48615  snlindsntor  48633  blen1b  48750  nn0sumshdiglem1  48783  0aryfvalel  48796  rrx2plordisom  48885  ehl2eudis0lt  48888  eenglngeehlnmlem2  48900  rrx2linest  48904  line2  48914  line2x  48916  line2y  48917  itschlc0xyqsol1  48928  itsclquadeu  48939  map0cor  49016  joindm2  49129  meetdm2  49131  islmd  49826  iscmd  49827