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 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  2reu4lem  4485  elimhyp3v  4556  elimhyp4v  4557  keephyp3v  4562  ralsng  4642  opeqsng  5488  snopeqop  5491  frsn  5751  f1eq123d  6814  foeq123d  6815  f1oeq123d  6816  fnmptfvd  7038  fnotovb  7464  ofrfvalg  7684  eloprabi  8061  fnmpoovd  8083  suppsnop  8175  smoeq  8338  naddasslem1  8682  naddasslem2  8683  mapsnend  9034  infglbb  9453  wemapwe  9667  fseqenlem1  10009  dfac12lem2  10129  fin23lem22  10312  pwfseqlem5  10649  pwfseq  10650  enqbreq2  10906  lterpq  10956  ltdiv23  12107  lediv23  12108  negfi  12165  halfpos  12475  addltmul  12481  div4p1lem1div2  12500  supminf  12960  supxrbnd1  13348  supxrbnd2  13349  iccf1o  13524  fzshftral  13645  fzoshftral  13818  2tnp1ge0ge0  13864  dfceil2  13874  modirr  13980  hashen1  14408  seqcoll  14503  hash2prb  14511  hashle2prv  14517  hash3tpb  14534  s111  14655  swrdspsleq  14705  pfxnd0  14728  pfxeq  14735  wrd2ind  14762  2swrd2eqwrdeq  14992  eqwrds3  15000  limsupgle  15530  tanaddlem  16223  difmod0  16346  dvdssub  16363  addmodlteqALT  16384  dvdsmod  16388  oddp1even  16403  nn0o1gt2  16440  nn0oddm1d2  16444  bitscmp  16497  saddisjlem  16523  smueqlem  16549  ncoprmgcdne1b  16709  cncongr1  16726  cncongr2  16727  prmreclem5  16981  4sqlem11  17016  4sqlem17  17022  vdwmc2  17040  ismre  17643  acsfn  17716  dfiso2  17830  brcic  17856  isssc  17878  setcinv  18148  cat1  18155  intopsn  18713  sgrp1  18788  sgrppropd  18790  sgrp2nmndlem4  18991  nmzsubg  19232  eqg0subg  19268  conjnmzb  19324  gsmsymgreqlem2  19502  symgfixels  19505  f1omvdconj  19517  oddvdsnn0  19615  oddvds  19618  odcong  19620  odf1  19633  dpjeq  20132  pgpfac1lem2  20148  isomnd  20194  ogrpinvlt  20215  ring1  20394  rngcinv  20723  ringcinv  20757  lsmspsn  21186  lbsacsbs  21261  rngqiprngimf1lem  21415  lpigen  21484  prmirredlem  21603  znf1o  21682  znleval  21685  znunit  21694  islinds2  21944  islindf4  21969  psdmul  22310  scmatf1  22669  isclo  23225  maxlp  23285  1stccn  23601  xkoinjcn  23825  elmptrab  23965  fbunfip  24007  elfm  24085  fmid  24098  flfnei  24129  isflf  24131  isfcls  24147  fclsopn  24152  isfcf  24172  cnextfun  24202  eltsms  24271  prdsxmetlem  24506  elmopn  24580  metss  24646  comet  24651  elbl4  24701  metuel2  24703  nrmmetd  24712  metdsge  24988  tcphcph  25377  fmcfil  25412  cmscsscms  25513  rrxmet  25548  minveclem4  25572  shft2rab  25648  sca2rab  25652  volsup2  25745  mbfsup  25804  i1fmullem  25834  mbfi1fseqlem4  25858  xrge0f  25871  itg2monolem1  25890  ellimc2  26017  cnlimc  26028  mdegleb  26202  r1pid2  26300  facth1  26305  ulm2  26529  sineq0  26670  coseq1  26671  efeq1  26674  sinord  26680  root1eq1  26901  angrtmuld  26954  affineequiv3  26971  quad2  26985  dcubic  26992  cubic2  26994  dquartlem1  26997  dquart  26999  quart  27007  rlimcnp  27111  lgamucov  27183  mumullem2  27325  chtub  27357  fsumvma  27358  fsumvma2  27359  chpchtsum  27364  dchrelbas2  27382  bposlem7  27435  lgsneg  27466  lgsne0  27480  lgsprme0  27484  lgsqrlem2  27492  lgsquadlem1  27525  lgsquadlem2  27526  2lgs  27552  2lgsoddprm  27561  2sqreultb  27604  lrrecval2  28114  subscan1d  28277  n0lesm1lt  28541  bdaypw2bnd  28639  elreno2  28669  istrkg3ld  28711  tgcgr4  28781  iscgra1  29102  isleag  29145  iseqlg  29165  axcontlem7  29301  elntg2  29316  edg0iedg0  29386  ausgrusgrb  29496  usgr1v0edg  29588  nb3grprlem2  29712  uvtx01vtx  29728  cplgr3v  29766  vtxd0nedgb  29819  vtxdusgr0edgnelALT  29827  1egrvtxdg0  29842  upgr2wlk  29997  wlkp1lem8  30009  dfpth2  30059  wwlksnextbi  30224  s3wwlks2on  30286  sps3wwlks2on  30287  elwwlks2  30299  elwspths2spth  30300  rusgrnumwwlkl1  30301  clwwlkwwlksb  30386  0pth  30457  upgriseupth  30539  eupth2lem2  30551  eupth2lem3lem4  30563  eupth2lem3lem6  30565  nfrgr2v  30604  frgr3v  30607  fusgr2wsp2nb  30666  fusgreg2wsp  30668  extwwlkfab  30684  numclwwlk2lem1  30708  frgrreggt1  30725  imsmetlem  31023  ipz  31052  bnsscmcl  31201  minvecolem4  31213  hvsubcan  31407  hoeq2  32164  leoptri  32469  atcv0eq  32712  elimifd  32870  fdifsupp  33011  ressupprn  33016  gtiso  33027  2ndpreima  33034  fpwrelmapffslem  33058  quad3d  33075  xnn01gt  33096  fzsplit3  33119  fzo0opth  33129  rlocisunit  33577  islinds5  33663  grplsmid  33694  selvply1rhmlem2  33892  fldextrspunlsp  34045  constrsuc  34109  smatrcl  34167  rhmpreimacnlem  34255  pstmfval  34267  lmlim  34318  dya2ub  34641  eulerpartlemr  34745  isrrvv  34814  ballotlemsima  34887  signsvfn  34950  subfacp1lem3  35655  subfacp1lem5  35657  erdszelem1  35664  erdsze  35675  erdsze2lem2  35677  satf0op  35850  fmlafvel  35858  isfmlasuc  35861  filnetlem4  36873  bj-issetwt  37491  bj-sbceqgALT  37518  bj-raldifsn  37723  bj-idreseq  37787  bj-elid6  37795  bj-imdirval3  37809  bj-imdirco  37815  poimirlem24  38276  itg2addnclem2  38304  ftc1anclem1  38325  areacirclem1  38340  areacirclem5  38344  metf1o  38387  isass  38478  rngosn3  38556  brxrn  39013  lsatcv0eq  39802  cmtbr2N  40008  atlatmstc  40074  1cvrco  40227  cdleme3  40992  cdleme7  41004  cdlemg10c  41394  dvhopellsm  41872  dibord  41914  dib1dim2  41923  diblsmopel  41926  dihopelvalcpre  42003  dih1dimatlem  42084  hdmap14lem13  42635  hdmapoc  42686  quadfac  42953  cxp112d  43083  cxp111d  43084  elrfirn  43409  jm2.19lem2  43700  pwfi2f1o  43806  proot1ex  43906  isoeq145d  44128  sqrtcval  44350  brfvidRP  44397  uneqsn  44734  ntrclsfveq  44771  ntrclskb  44778  ntrclsk3  44779  ntrneiel2  44795  k0004lem3  44858  bcc0  45033  pwpwuni  45760  disjinfi  45893  rnmptbd2  45947  rnmptbd  45954  infxrbnd2  46067  ltmulneg  46090  ltdiv23neg  46092  rexabsle  46116  uzub  46128  supxrleubrnmptf  46148  supminfxr  46161  limsupre2lem  46421  limsupre2mpt  46427  limsupre3mpt  46431  limsupreuz  46434  limsuplt2  46450  liminflimsupclim  46504  xlimpnfxnegmnf  46511  liminfpnfuz  46513  xlimclim  46521  xlimbr  46524  xlimclim2lem  46536  xlimmnfmpt  46540  xlimpnfmpt  46541  fourierdlem113  46916  isvonmbl  47335  chnsubseqwl  47578  reuf1odnf  47827  addsubeq0  48016  ltnltne  48019  ceilbi  48057  iccpartgtl  48158  iccpartleu  48160  iccpartgel  48161  reuprpr  48255  fmtnoprmfac1  48300  fmtnoprmfac2  48302  quad1  48368  requad1  48370  requad2  48371  bits0ALTV  48427  bgoldbtbndlem1  48553  clnbgrel  48576  clnbupgrel  48582  dfsclnbgr6  48606  isubgredg  48614  gpgiedgdmel  48797  opgpgvtx  48803  gpg3kgrtriexlem5  48835  0nodd  48918  2nodd  48920  rngcinvALTV  49024  ringcinvALTV  49058  crngprmringidom  49089  islindeps  49216  snlindsntor  49234  blen1b  49351  nn0sumshdiglem1  49384  0aryfvalel  49397  rrx2plordisom  49486  ehl2eudis0lt  49489  eenglngeehlnmlem2  49501  rrx2linest  49505  line2  49515  line2x  49517  line2y  49518  itschlc0xyqsol1  49529  itsclquadeu  49540  map0cor  49616  joindm2  49729  meetdm2  49731  islmd  50426  iscmd  50427