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  4476  elimhyp3v  4547  elimhyp4v  4548  keephyp3v  4553  ralsng  4632  opeqsng  5451  snopeqop  5454  frsn  5712  f1eq123d  6766  foeq123d  6767  f1oeq123d  6768  fnmptfvd  6986  fnotovb  7410  ofrfvalg  7630  eloprabi  8007  fnmpoovd  8029  suppsnop  8120  smoeq  8282  naddasslem1  8622  naddasslem2  8623  mapsnend  8973  infglbb  9395  wemapwe  9606  fseqenlem1  9934  dfac12lem2  10055  fin23lem22  10237  pwfseqlem5  10574  pwfseq  10575  enqbreq2  10831  lterpq  10881  ltdiv23  12033  lediv23  12034  negfi  12091  halfpos  12371  addltmul  12377  div4p1lem1div2  12396  supminf  12848  supxrbnd1  13236  supxrbnd2  13237  iccf1o  13412  fzshftral  13531  fzoshftral  13703  2tnp1ge0ge0  13749  dfceil2  13759  modirr  13865  hashen1  14293  seqcoll  14387  hash2prb  14395  hashle2prv  14401  hash3tpb  14418  s111  14539  swrdspsleq  14589  pfxnd0  14612  pfxeq  14619  wrd2ind  14646  2swrd2eqwrdeq  14876  eqwrds3  14884  limsupgle  15400  tanaddlem  16091  difmod0  16214  dvdssub  16231  addmodlteqALT  16252  dvdsmod  16256  oddp1even  16271  nn0o1gt2  16308  nn0oddm1d2  16312  bitscmp  16365  saddisjlem  16391  smueqlem  16417  ncoprmgcdne1b  16577  cncongr1  16594  cncongr2  16595  prmreclem5  16848  4sqlem11  16883  4sqlem17  16889  vdwmc2  16907  ismre  17509  acsfn  17582  dfiso2  17696  brcic  17722  isssc  17744  setcinv  18014  cat1  18021  intopsn  18579  sgrp1  18654  sgrppropd  18656  sgrp2nmndlem4  18853  nmzsubg  19094  eqg0subg  19125  conjnmzb  19182  gsmsymgreqlem2  19360  symgfixels  19363  f1omvdconj  19375  oddvdsnn0  19473  oddvds  19476  odcong  19478  odf1  19491  dpjeq  19990  pgpfac1lem2  20006  isomnd  20052  ogrpinvlt  20073  ring1  20245  rngcinv  20570  ringcinv  20604  lsmspsn  21036  lbsacsbs  21111  rngqiprngimf1lem  21249  lpigen  21290  prmirredlem  21427  znf1o  21506  znleval  21509  znunit  21518  islinds2  21768  islindf4  21793  psdmul  22109  scmatf1  22475  isclo  23031  maxlp  23091  1stccn  23407  xkoinjcn  23631  elmptrab  23771  fbunfip  23813  elfm  23891  fmid  23904  flfnei  23935  isflf  23937  isfcls  23953  fclsopn  23958  isfcf  23978  cnextfun  24008  eltsms  24077  prdsxmetlem  24312  elmopn  24386  metss  24452  comet  24457  elbl4  24507  metuel2  24509  nrmmetd  24518  metdsge  24794  tcphcph  25193  fmcfil  25228  cmscsscms  25329  rrxmet  25364  minveclem4  25388  shft2rab  25465  sca2rab  25469  volsup2  25562  mbfsup  25621  i1fmullem  25651  mbfi1fseqlem4  25675  xrge0f  25688  itg2monolem1  25707  ellimc2  25834  cnlimc  25845  mdegleb  26025  r1pid2  26123  facth1  26128  ulm2  26350  sineq0  26489  coseq1  26490  efeq1  26493  sinord  26499  root1eq1  26721  angrtmuld  26774  affineequiv3  26791  quad2  26805  dcubic  26812  cubic2  26814  dquartlem1  26817  dquart  26819  quart  26827  rlimcnp  26931  lgamucov  27004  mumullem2  27146  chtub  27179  fsumvma  27180  fsumvma2  27181  chpchtsum  27186  dchrelbas2  27204  bposlem7  27257  lgsneg  27288  lgsne0  27302  lgsprme0  27306  lgsqrlem2  27314  lgsquadlem1  27347  lgsquadlem2  27348  2lgs  27374  2lgsoddprm  27383  2sqreultb  27426  lrrecval2  27936  subscan1d  28099  n0lesm1lt  28363  bdaypw2bnd  28461  elreno2  28491  istrkg3ld  28533  tgcgr4  28603  iscgra1  28882  isleag  28919  iseqlg  28939  axcontlem7  29043  elntg2  29058  edg0iedg0  29128  ausgrusgrb  29238  usgr1v0edg  29330  nb3grprlem2  29454  uvtx01vtx  29470  cplgr3v  29508  vtxd0nedgb  29562  vtxdusgr0edgnelALT  29570  1egrvtxdg0  29585  upgr2wlk  29740  wlkp1lem8  29752  dfpth2  29802  wwlksnextbi  29967  s3wwlks2on  30029  sps3wwlks2on  30030  elwwlks2  30042  elwspths2spth  30043  rusgrnumwwlkl1  30044  clwwlkwwlksb  30129  0pth  30200  upgriseupth  30282  eupth2lem2  30294  eupth2lem3lem4  30306  eupth2lem3lem6  30308  nfrgr2v  30347  frgr3v  30350  fusgr2wsp2nb  30409  fusgreg2wsp  30411  extwwlkfab  30427  numclwwlk2lem1  30451  frgrreggt1  30468  imsmetlem  30765  ipz  30794  bnsscmcl  30943  minvecolem4  30955  hvsubcan  31149  hoeq2  31906  leoptri  32211  atcv0eq  32454  elimifd  32618  fdifsupp  32764  ressupprn  32769  gtiso  32780  2ndpreima  32787  fpwrelmapffslem  32811  quad3d  32829  xnn01gt  32850  fzsplit3  32873  fzo0opth  32883  islinds5  33448  grplsmid  33485  r1pid2OLD  33690  fldextrspunlsp  33831  constrsuc  33895  smatrcl  33953  rhmpreimacnlem  34041  pstmfval  34053  lmlim  34104  dya2ub  34427  eulerpartlemr  34531  isrrvv  34600  ballotlemsima  34673  signsvfn  34739  subfacp1lem3  35376  subfacp1lem5  35378  erdszelem1  35385  erdsze  35396  erdsze2lem2  35398  satf0op  35571  fmlafvel  35579  isfmlasuc  35582  filnetlem4  36575  bj-issetwt  37076  bj-sbceqgALT  37103  bj-raldifsn  37305  bj-idreseq  37367  bj-elid6  37375  bj-imdirval3  37389  bj-imdirco  37395  poimirlem24  37845  itg2addnclem2  37873  ftc1anclem1  37894  areacirclem1  37909  areacirclem5  37913  metf1o  37956  isass  38047  rngosn3  38125  brxrn  38568  lsatcv0eq  39307  cmtbr2N  39513  atlatmstc  39579  1cvrco  39732  cdleme3  40497  cdleme7  40509  cdlemg10c  40899  dvhopellsm  41377  dibord  41419  dib1dim2  41428  diblsmopel  41431  dihopelvalcpre  41508  dih1dimatlem  41589  hdmap14lem13  42140  hdmapoc  42191  cxp112d  42596  cxp111d  42597  elrfirn  42937  jm2.19lem2  43232  pwfi2f1o  43338  proot1ex  43438  isoeq145d  43660  sqrtcval  43882  brfvidRP  43929  uneqsn  44266  ntrclsfveq  44303  ntrclskb  44310  ntrclsk3  44311  ntrneiel2  44327  k0004lem3  44390  bcc0  44581  pwpwuni  45302  disjinfi  45436  rnmptbd2  45493  rnmptbd  45500  infxrbnd2  45613  ltmulneg  45636  ltdiv23neg  45638  rexabsle  45663  uzub  45675  supxrleubrnmptf  45695  supminfxr  45708  limsupre2lem  45968  limsupre2mpt  45974  limsupre3mpt  45978  limsupreuz  45981  limsuplt2  45997  liminflimsupclim  46051  xlimpnfxnegmnf  46058  liminfpnfuz  46060  xlimclim  46068  xlimbr  46071  xlimclim2lem  46083  xlimmnfmpt  46087  xlimpnfmpt  46088  fourierdlem113  46463  isvonmbl  46882  chnsubseqwl  47123  reuf1odnf  47353  addsubeq0  47542  ltnltne  47545  ceilbi  47579  iccpartgtl  47672  iccpartleu  47674  iccpartgel  47675  reuprpr  47769  fmtnoprmfac1  47811  fmtnoprmfac2  47813  quad1  47866  requad1  47868  requad2  47869  bits0ALTV  47925  bgoldbtbndlem1  48051  clnbgrel  48074  clnbupgrel  48080  dfsclnbgr6  48104  isubgredg  48112  gpgiedgdmel  48295  opgpgvtx  48301  gpg3kgrtriexlem5  48333  0nodd  48416  2nodd  48418  rngcinvALTV  48522  ringcinvALTV  48556  islindeps  48699  snlindsntor  48717  blen1b  48834  nn0sumshdiglem1  48867  0aryfvalel  48880  rrx2plordisom  48969  ehl2eudis0lt  48972  eenglngeehlnmlem2  48984  rrx2linest  48988  line2  48998  line2x  49000  line2y  49001  itschlc0xyqsol1  49012  itsclquadeu  49023  map0cor  49100  joindm2  49213  meetdm2  49215  islmd  49910  iscmd  49911