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  4463  elimhyp3v  4534  elimhyp4v  4535  keephyp3v  4540  ralsng  4619  opeqsng  5457  snopeqop  5460  frsn  5719  f1eq123d  6772  foeq123d  6773  f1oeq123d  6774  fnmptfvd  6993  fnotovb  7419  ofrfvalg  7639  eloprabi  8016  fnmpoovd  8037  suppsnop  8128  smoeq  8290  naddasslem1  8630  naddasslem2  8631  mapsnend  8983  infglbb  9405  wemapwe  9618  fseqenlem1  9946  dfac12lem2  10067  fin23lem22  10249  pwfseqlem5  10586  pwfseq  10587  enqbreq2  10843  lterpq  10893  ltdiv23  12047  lediv23  12048  negfi  12105  halfpos  12407  addltmul  12413  div4p1lem1div2  12432  supminf  12885  supxrbnd1  13273  supxrbnd2  13274  iccf1o  13449  fzshftral  13569  fzoshftral  13742  2tnp1ge0ge0  13788  dfceil2  13798  modirr  13904  hashen1  14332  seqcoll  14426  hash2prb  14434  hashle2prv  14440  hash3tpb  14457  s111  14578  swrdspsleq  14628  pfxnd0  14651  pfxeq  14658  wrd2ind  14685  2swrd2eqwrdeq  14915  eqwrds3  14923  limsupgle  15439  tanaddlem  16133  difmod0  16256  dvdssub  16273  addmodlteqALT  16294  dvdsmod  16298  oddp1even  16313  nn0o1gt2  16350  nn0oddm1d2  16354  bitscmp  16407  saddisjlem  16433  smueqlem  16459  ncoprmgcdne1b  16619  cncongr1  16636  cncongr2  16637  prmreclem5  16891  4sqlem11  16926  4sqlem17  16932  vdwmc2  16950  ismre  17552  acsfn  17625  dfiso2  17739  brcic  17765  isssc  17787  setcinv  18057  cat1  18064  intopsn  18622  sgrp1  18697  sgrppropd  18699  sgrp2nmndlem4  18899  nmzsubg  19140  eqg0subg  19171  conjnmzb  19228  gsmsymgreqlem2  19406  symgfixels  19409  f1omvdconj  19421  oddvdsnn0  19519  oddvds  19522  odcong  19524  odf1  19537  dpjeq  20036  pgpfac1lem2  20052  isomnd  20098  ogrpinvlt  20119  ring1  20291  rngcinv  20614  ringcinv  20648  lsmspsn  21079  lbsacsbs  21154  rngqiprngimf1lem  21292  lpigen  21333  prmirredlem  21452  znf1o  21531  znleval  21534  znunit  21543  islinds2  21793  islindf4  21818  psdmul  22132  scmatf1  22496  isclo  23052  maxlp  23112  1stccn  23428  xkoinjcn  23652  elmptrab  23792  fbunfip  23834  elfm  23912  fmid  23925  flfnei  23956  isflf  23958  isfcls  23974  fclsopn  23979  isfcf  23999  cnextfun  24029  eltsms  24098  prdsxmetlem  24333  elmopn  24407  metss  24473  comet  24478  elbl4  24528  metuel2  24530  nrmmetd  24539  metdsge  24815  tcphcph  25204  fmcfil  25239  cmscsscms  25340  rrxmet  25375  minveclem4  25399  shft2rab  25475  sca2rab  25479  volsup2  25572  mbfsup  25631  i1fmullem  25661  mbfi1fseqlem4  25685  xrge0f  25698  itg2monolem1  25717  ellimc2  25844  cnlimc  25855  mdegleb  26029  r1pid2  26127  facth1  26132  ulm2  26350  sineq0  26488  coseq1  26489  efeq1  26492  sinord  26498  root1eq1  26719  angrtmuld  26772  affineequiv3  26789  quad2  26803  dcubic  26810  cubic2  26812  dquartlem1  26815  dquart  26817  quart  26825  rlimcnp  26929  lgamucov  27001  mumullem2  27143  chtub  27175  fsumvma  27176  fsumvma2  27177  chpchtsum  27182  dchrelbas2  27200  bposlem7  27253  lgsneg  27284  lgsne0  27298  lgsprme0  27302  lgsqrlem2  27310  lgsquadlem1  27343  lgsquadlem2  27344  2lgs  27370  2lgsoddprm  27379  2sqreultb  27422  lrrecval2  27932  subscan1d  28095  n0lesm1lt  28359  bdaypw2bnd  28457  elreno2  28487  istrkg3ld  28529  tgcgr4  28599  iscgra1  28878  isleag  28915  iseqlg  28935  axcontlem7  29039  elntg2  29054  edg0iedg0  29124  ausgrusgrb  29234  usgr1v0edg  29326  nb3grprlem2  29450  uvtx01vtx  29466  cplgr3v  29504  vtxd0nedgb  29557  vtxdusgr0edgnelALT  29565  1egrvtxdg0  29580  upgr2wlk  29735  wlkp1lem8  29747  dfpth2  29797  wwlksnextbi  29962  s3wwlks2on  30024  sps3wwlks2on  30025  elwwlks2  30037  elwspths2spth  30038  rusgrnumwwlkl1  30039  clwwlkwwlksb  30124  0pth  30195  upgriseupth  30277  eupth2lem2  30289  eupth2lem3lem4  30301  eupth2lem3lem6  30303  nfrgr2v  30342  frgr3v  30345  fusgr2wsp2nb  30404  fusgreg2wsp  30406  extwwlkfab  30422  numclwwlk2lem1  30446  frgrreggt1  30463  imsmetlem  30761  ipz  30790  bnsscmcl  30939  minvecolem4  30951  hvsubcan  31145  hoeq2  31902  leoptri  32207  atcv0eq  32450  elimifd  32613  fdifsupp  32758  ressupprn  32763  gtiso  32774  2ndpreima  32781  fpwrelmapffslem  32805  quad3d  32822  xnn01gt  32843  fzsplit3  32866  fzo0opth  32876  islinds5  33427  grplsmid  33464  r1pid2OLD  33669  fldextrspunlsp  33818  constrsuc  33882  smatrcl  33940  rhmpreimacnlem  34028  pstmfval  34040  lmlim  34091  dya2ub  34414  eulerpartlemr  34518  isrrvv  34587  ballotlemsima  34660  signsvfn  34726  subfacp1lem3  35364  subfacp1lem5  35366  erdszelem1  35373  erdsze  35384  erdsze2lem2  35386  satf0op  35559  fmlafvel  35567  isfmlasuc  35570  filnetlem4  36563  bj-issetwt  37182  bj-sbceqgALT  37209  bj-raldifsn  37412  bj-idreseq  37476  bj-elid6  37484  bj-imdirval3  37498  bj-imdirco  37504  poimirlem24  37965  itg2addnclem2  37993  ftc1anclem1  38014  areacirclem1  38029  areacirclem5  38033  metf1o  38076  isass  38167  rngosn3  38245  brxrn  38704  lsatcv0eq  39493  cmtbr2N  39699  atlatmstc  39765  1cvrco  39918  cdleme3  40683  cdleme7  40695  cdlemg10c  41085  dvhopellsm  41563  dibord  41605  dib1dim2  41614  diblsmopel  41617  dihopelvalcpre  41694  dih1dimatlem  41775  hdmap14lem13  42326  hdmapoc  42377  cxp112d  42773  cxp111d  42774  elrfirn  43127  jm2.19lem2  43418  pwfi2f1o  43524  proot1ex  43624  isoeq145d  43846  sqrtcval  44068  brfvidRP  44115  uneqsn  44452  ntrclsfveq  44489  ntrclskb  44496  ntrclsk3  44497  ntrneiel2  44513  k0004lem3  44576  bcc0  44767  pwpwuni  45488  disjinfi  45622  rnmptbd2  45678  rnmptbd  45685  infxrbnd2  45798  ltmulneg  45821  ltdiv23neg  45823  rexabsle  45847  uzub  45859  supxrleubrnmptf  45879  supminfxr  45892  limsupre2lem  46152  limsupre2mpt  46158  limsupre3mpt  46162  limsupreuz  46165  limsuplt2  46181  liminflimsupclim  46235  xlimpnfxnegmnf  46242  liminfpnfuz  46244  xlimclim  46252  xlimbr  46255  xlimclim2lem  46267  xlimmnfmpt  46271  xlimpnfmpt  46272  fourierdlem113  46647  isvonmbl  47066  chnsubseqwl  47309  reuf1odnf  47555  addsubeq0  47744  ltnltne  47747  ceilbi  47785  iccpartgtl  47886  iccpartleu  47888  iccpartgel  47889  reuprpr  47983  fmtnoprmfac1  48028  fmtnoprmfac2  48030  quad1  48096  requad1  48098  requad2  48099  bits0ALTV  48155  bgoldbtbndlem1  48281  clnbgrel  48304  clnbupgrel  48310  dfsclnbgr6  48334  isubgredg  48342  gpgiedgdmel  48525  opgpgvtx  48531  gpg3kgrtriexlem5  48563  0nodd  48646  2nodd  48648  rngcinvALTV  48752  ringcinvALTV  48786  islindeps  48929  snlindsntor  48947  blen1b  49064  nn0sumshdiglem1  49097  0aryfvalel  49110  rrx2plordisom  49199  ehl2eudis0lt  49202  eenglngeehlnmlem2  49214  rrx2linest  49218  line2  49228  line2x  49230  line2y  49231  itschlc0xyqsol1  49242  itsclquadeu  49253  map0cor  49330  joindm2  49443  meetdm2  49445  islmd  50140  iscmd  50141