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 205

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 206

This theorem is referenced by:  sbceqalOLD  3844  2reu4lem  4525  elimhyp3v  4595  elimhyp4v  4596  keephyp3v  4601  ralsng  4677  opeqsng  5503  snopeqop  5506  frsn  5762  f1eq123d  6823  foeq123d  6824  f1oeq123d  6825  fnmptfvd  7040  fnotovb  7456  ofrfvalg  7675  eloprabi  8046  fnmpoovd  8070  suppsnop  8160  smoeq  8347  naddasslem1  8690  naddasslem2  8691  mapsnend  9033  infglbb  9483  wemapwe  9689  fseqenlem1  10016  dfac12lem2  10136  fin23lem22  10319  pwfseqlem5  10655  pwfseq  10656  enqbreq2  10912  lterpq  10962  ltdiv23  12102  lediv23  12103  negfi  12160  halfpos  12439  addltmul  12445  div4p1lem1div2  12464  supminf  12916  supxrbnd1  13297  supxrbnd2  13298  iccf1o  13470  fzshftral  13586  fzoshftral  13746  2tnp1ge0ge0  13791  dfceil2  13801  modirr  13904  hashen1  14327  seqcoll  14422  hash2prb  14430  hashle2prv  14436  s111  14562  swrdspsleq  14612  pfxnd0  14635  pfxeq  14643  wrd2ind  14670  2swrd2eqwrdeq  14901  eqwrds3  14909  limsupgle  15418  tanaddlem  16106  dvdssub  16244  addmodlteqALT  16265  dvdsmod  16269  oddp1even  16284  nn0o1gt2  16321  nn0oddm1d2  16325  bitscmp  16376  saddisjlem  16402  smueqlem  16428  ncoprmgcdne1b  16584  cncongr1  16601  cncongr2  16602  prmreclem5  16850  4sqlem11  16885  4sqlem17  16891  vdwmc2  16909  ismre  17531  acsfn  17600  dfiso2  17716  brcic  17742  isssc  17764  setcinv  18037  cat1  18044  intopsn  18570  sgrp1  18617  sgrppropd  18619  sgrp2nmndlem4  18806  nmzsubg  19040  eqg0subg  19068  conjnmzb  19122  gsmsymgreqlem2  19294  symgfixels  19297  f1omvdconj  19309  oddvdsnn0  19407  oddvds  19410  odcong  19412  odf1  19425  dpjeq  19924  pgpfac1lem2  19940  ring1  20116  lsmspsn  20688  lbsacsbs  20762  df2idl2  20853  lpigen  20887  prmirredlem  21034  znf1o  21099  znleval  21102  znunit  21111  islinds2  21360  islindf4  21385  scmatf1  22025  isclo  22583  maxlp  22643  1stccn  22959  xkoinjcn  23183  elmptrab  23323  fbunfip  23365  elfm  23443  fmid  23456  flfnei  23487  isflf  23489  isfcls  23505  fclsopn  23510  isfcf  23530  cnextfun  23560  eltsms  23629  prdsxmetlem  23866  elmopn  23940  metss  24009  comet  24014  elbl4  24064  metuel2  24066  nrmmetd  24075  metdsge  24357  tcphcph  24746  fmcfil  24781  cmscsscms  24882  rrxmet  24917  minveclem4  24941  shft2rab  25017  sca2rab  25021  volsup2  25114  mbfsup  25173  i1fmullem  25203  mbfi1fseqlem4  25228  xrge0f  25241  itg2monolem1  25260  ellimc2  25386  cnlimc  25397  mdegleb  25574  facth1  25674  ulm2  25889  sineq0  26025  coseq1  26026  efeq1  26029  sinord  26035  root1eq1  26253  angrtmuld  26303  affineequiv3  26320  quad2  26334  dcubic  26341  cubic2  26343  dquartlem1  26346  dquart  26348  quart  26356  rlimcnp  26460  lgamucov  26532  mumullem2  26674  chtub  26705  fsumvma  26706  fsumvma2  26707  chpchtsum  26712  dchrelbas2  26730  bposlem7  26783  lgsneg  26814  lgsne0  26828  lgsprme0  26832  lgsqrlem2  26840  lgsquadlem1  26873  lgsquadlem2  26874  2lgs  26900  2lgsoddprm  26909  2sqreultb  26952  lrrecval2  27414  istrkg3ld  27702  tgcgr4  27772  iscgra1  28051  isleag  28088  iseqlg  28108  axcontlem7  28218  elntg2  28233  edg0iedg0  28305  ausgrusgrb  28415  usgr1v0edg  28504  nb3grprlem2  28628  uvtx01vtx  28644  cplgr3v  28682  vtxd0nedgb  28735  vtxdusgr0edgnelALT  28743  1egrvtxdg0  28758  upgr2wlk  28915  wlkp1lem8  28927  wwlksnextbi  29138  s3wwlks2on  29200  elwwlks2  29210  elwspths2spth  29211  rusgrnumwwlkl1  29212  clwwlkwwlksb  29297  0pth  29368  upgriseupth  29450  eupth2lem2  29462  eupth2lem3lem4  29474  eupth2lem3lem6  29476  nfrgr2v  29515  frgr3v  29518  fusgr2wsp2nb  29577  fusgreg2wsp  29579  extwwlkfab  29595  numclwwlk2lem1  29619  frgrreggt1  29636  imsmetlem  29931  ipz  29960  bnsscmcl  30109  minvecolem4  30121  hvsubcan  30315  hoeq2  31072  leoptri  31377  atcv0eq  31620  elimifd  31763  ressupprn  31900  gtiso  31910  2ndpreima  31917  fpwrelmapffslem  31945  xnn01gt  31971  fzsplit3  31993  isomnd  32207  ogrpinvlt  32229  islinds5  32469  grplsmid  32503  smatrcl  32765  rhmpreimacnlem  32853  pstmfval  32865  lmlim  32916  dya2ub  33258  eulerpartlemr  33362  isrrvv  33431  ballotlemsima  33503  signsvfn  33582  subfacp1lem3  34162  subfacp1lem5  34164  erdszelem1  34171  erdsze  34182  erdsze2lem2  34184  satf0op  34357  fmlafvel  34365  isfmlasuc  34368  filnetlem4  35255  bj-issetwt  35743  bj-sbceqgALT  35771  bj-raldifsn  35970  bj-idreseq  36032  bj-elid6  36040  bj-imdirval3  36054  bj-imdirco  36060  poimirlem24  36501  itg2addnclem2  36529  ftc1anclem1  36550  areacirclem1  36565  areacirclem5  36569  metf1o  36612  isass  36703  rngosn3  36781  brxrn  37233  lsatcv0eq  37906  cmtbr2N  38112  atlatmstc  38178  1cvrco  38332  cdleme3  39097  cdleme7  39109  cdlemg10c  39499  dvhopellsm  39977  dibord  40019  dib1dim2  40028  diblsmopel  40031  dihopelvalcpre  40108  dih1dimatlem  40189  hdmap14lem13  40740  hdmapoc  40791  elrfirn  41419  jm2.19lem2  41715  pwfi2f1o  41824  proot1ex  41929  isoeq145d  42156  sqrtcval  42378  brfvidRP  42425  uneqsn  42762  ntrclsfveq  42799  ntrclskb  42806  ntrclsk3  42807  ntrneiel2  42823  k0004lem3  42886  bcc0  43085  pwpwuni  43730  disjinfi  43877  rnmptbd2  43940  rnmptbd  43947  infxrbnd2  44066  ltmulneg  44089  ltdiv23neg  44091  rexabsle  44116  uzub  44128  supxrleubrnmptf  44148  supminfxr  44161  limsupre2lem  44427  limsupre2mpt  44433  limsupre3mpt  44437  limsupreuz  44440  limsuplt2  44456  liminflimsupclim  44510  xlimpnfxnegmnf  44517  liminfpnfuz  44519  xlimclim  44527  xlimbr  44530  xlimclim2lem  44542  xlimmnfmpt  44546  xlimpnfmpt  44547  fourierdlem113  44922  isvonmbl  45341  reuf1odnf  45802  addsubeq0  45991  ltnltne  45994  iccpartgtl  46081  iccpartleu  46083  iccpartgel  46084  reuprpr  46178  fmtnoprmfac1  46220  fmtnoprmfac2  46222  quad1  46275  requad1  46277  requad2  46278  bits0ALTV  46334  bgoldbtbndlem1  46460  0nodd  46567  2nodd  46569  rngqiprngimf1lem  46760  rngcinv  46833  rngcinvALTV  46845  ringcinv  46884  ringcinvALTV  46908  islindeps  47088  snlindsntor  47106  blen1b  47228  nn0sumshdiglem1  47261  0aryfvalel  47274  rrx2plordisom  47363  ehl2eudis0lt  47366  eenglngeehlnmlem2  47378  rrx2linest  47382  line2  47392  line2x  47394  line2y  47395  itschlc0xyqsol1  47406  itsclquadeu  47417  map0cor  47475  joindm2  47555  meetdm2  47557