Theorem 3bitrd 306

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 280	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 280	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  sbceqal  3763  2reu4lem  4379  elimhyp3v  4446  elimhyp4v  4447  keephyp3v  4452  opeqsng  5284  snopeqop  5287  frsn  5525  elpredg  6037  f1eq123d  6476  foeq123d  6477  f1oeq123d  6478  fnmptfvd  6676  fnotovb  7065  ofrfval  7275  eloprabi  7617  fnmpoovd  7638  suppsnop  7695  smoeq  7839  mapsnend  8436  infglbb  8801  wemapwe  9006  fseqenlem1  9296  dfac12lem2  9416  fin23lem22  9595  pwfseqlem5  9931  pwfseq  9932  enqbreq2  10188  lterpq  10238  ltdiv23  11379  lediv23  11380  negfi  11437  halfpos  11715  addltmul  11721  div4p1lem1div2  11740  supminf  12184  supxrbnd1  12564  supxrbnd2  12565  iccf1o  12732  fzshftral  12845  fzoshftral  13004  2tnp1ge0ge0  13049  dfceil2  13059  modirr  13160  hashen1  13580  seqcoll  13670  hash2prb  13676  hashle2prv  13682  ccat0  13774  s111  13813  pfxnd0  13886  pfxeq  13894  wrd2ind  13921  2swrd2eqwrdeq  14151  eqwrds3  14159  limsupgle  14668  tanaddlem  15352  dvdssub  15487  addmodlteqALT  15508  dvdsmod  15511  oddp1even  15526  nn0o1gt2  15565  nn0oddm1d2  15569  bitscmp  15620  saddisjlem  15646  smueqlem  15672  ncoprmgcdne1b  15823  cncongr1  15840  cncongr2  15841  prmreclem5  16085  4sqlem11  16120  4sqlem17  16126  vdwmc2  16144  ismre  16690  acsfn  16759  dfiso2  16871  brcic  16897  isssc  16919  setcinv  17179  intopsn  17692  sgrp1  17732  sgrp2nmndlem4  17854  nmzsubg  18074  conjnmzb  18134  gsmsymgreqlem2  18290  symgfixels  18293  f1omvdconj  18305  oddvdsnn0  18403  oddvds  18406  odcong  18408  odf1  18419  dpjeq  18898  pgpfac1lem2  18914  ring1  19042  lsmspsn  19546  lbsacsbs  19618  lpigen  19718  prmirredlem  20322  znf1o  20380  znleval  20383  znunit  20392  islinds2  20639  islindf4  20664  scmatf1  20824  isclo  21379  maxlp  21439  1stccn  21755  xkoinjcn  21979  elmptrab  22119  fbunfip  22161  elfm  22239  fmid  22252  flfnei  22283  isflf  22285  isfcls  22301  fclsopn  22306  isfcf  22326  cnextfun  22356  eltsms  22424  prdsxmetlem  22661  elmopn  22735  metss  22801  comet  22806  elbl4  22856  metuel2  22858  nrmmetd  22867  metdsge  23140  tcphcph  23523  fmcfil  23558  cmscsscms  23659  rrxmet  23694  minveclem4  23718  shft2rab  23792  sca2rab  23796  volsup2  23889  mbfsup  23948  i1fmullem  23978  mbfi1fseqlem4  24002  xrge0f  24015  itg2monolem1  24034  ellimc2  24158  cnlimc  24169  mdegleb  24341  facth1  24441  ulm2  24656  sineq0  24792  coseq1  24793  efeq1  24794  sinord  24799  root1eq1  25017  angrtmuld  25067  affineequiv3  25084  quad2  25098  dcubic  25105  cubic2  25107  dquartlem1  25110  dquart  25112  quart  25120  rlimcnp  25225  lgamucov  25297  mumullem2  25439  chtub  25470  fsumvma  25471  fsumvma2  25472  chpchtsum  25477  dchrelbas2  25495  bposlem7  25548  lgsneg  25579  lgsne0  25593  lgsprme0  25597  lgsqrlem2  25605  lgsquadlem1  25638  lgsquadlem2  25639  2lgs  25665  2lgsoddprm  25674  2sqreultb  25717  istrkg3ld  25929  tgcgr4  25999  iscgra1  26278  isleag  26316  iseqlg  26336  axcontlem7  26439  elntg2  26454  edg0iedg0  26523  ausgrusgrb  26633  usgr1v0edg  26722  nb3grprlem2  26846  uvtx01vtx  26862  cplgr3v  26900  vtxd0nedgb  26953  vtxdusgr0edgnelALT  26961  1egrvtxdg0  26976  wlkeq  27098  upgr2wlk  27132  wlkp1lem8  27147  wwlksnextbi  27359  s3wwlks2on  27422  elwwlks2  27432  elwspths2spth  27433  rusgrnumwwlkl1  27434  clwwlkwwlksb  27520  0pth  27591  upgriseupth  27673  eupth2lem2  27686  eupth2lem3lem4  27698  eupth2lem3lem6  27700  nfrgr2v  27743  frgr3v  27746  fusgr2wsp2nb  27805  fusgreg2wsp  27807  extwwlkfab  27823  numclwwlk2lem1  27847  frgrreggt1  27864  imsmetlem  28158  ipz  28187  bnsscmcl  28336  minvecolem4  28348  hvsubcan  28542  hoeq2  29299  leoptri  29604  atcv0eq  29847  elimifd  29987  gtiso  30124  2ndpreima  30131  fpwrelmapffslem  30156  xnn01gt  30183  fzsplit3  30203  isomnd  30362  ogrpinvlt  30384  islinds5  30580  smatrcl  30676  pstmfval  30753  lmlim  30807  dya2ub  31145  eulerpartlemr  31249  isrrvv  31318  ballotlemsima  31390  signsvfn  31469  subfacp1lem3  32037  subfacp1lem5  32039  erdszelem1  32046  erdsze  32057  erdsze2lem2  32059  satf0op  32232  fmlafvel  32240  isfmlasuc  32243  filnetlem4  33338  bj-issetwt  33761  bj-sbceqgALT  33790  bj-raldifsn  33991  csbwrecsg  34139  poimirlem24  34447  itg2addnclem2  34475  ftc1anclem1  34498  areacirclem1  34513  areacirclem5  34517  metf1o  34562  isass  34656  rngosn3  34734  brxrn  35157  lsatcv0eq  35714  cmtbr2N  35920  atlatmstc  35986  1cvrco  36139  cdleme3  36904  cdleme7  36916  cdlemg10c  37306  dvhopellsm  37784  dibord  37826  dib1dim2  37835  diblsmopel  37838  dihopelvalcpre  37915  dih1dimatlem  37996  hdmap14lem13  38547  hdmapoc  38598  elrfirn  38777  jm2.19lem2  39072  pwfi2f1o  39181  proot1ex  39286  brfvidRP  39518  uneqsn  39858  ntrclsfveq  39897  ntrclskb  39904  ntrclsk3  39905  ntrneiel2  39921  k0004lem3  39984  bcc0  40210  pwpwuni  40858  disjinfi  40994  rnmptbd2  41062  rnmptbd  41069  infxrbnd2  41178  ltmulneg  41205  ltdiv23neg  41207  rexabsle  41235  uzub  41247  supxrleubrnmptf  41269  supminfxr  41282  limsupre2lem  41547  limsupre2mpt  41553  limsupre3mpt  41557  limsupreuz  41560  limsuplt2  41576  liminflimsupclim  41630  xlimpnfxnegmnf  41637  liminfpnfuz  41639  xlimclim  41647  xlimbr  41650  xlimclim2lem  41662  xlimmnfmpt  41666  xlimpnfmpt  41667  fourierdlem113  42046  isvonmbl  42462  reuf1odnf  42822  addsubeq0  43012  ltnltne  43015  iccpartgtl  43068  iccpartleu  43070  iccpartgel  43071  reuprpr  43167  fmtnoprmfac1  43209  fmtnoprmfac2  43211  quad1  43267  requad1  43269  requad2  43270  bits0ALTV  43326  bgoldbtbndlem1  43452  0nodd  43559  2nodd  43561  rngcinv  43730  rngcinvALTV  43742  ringcinv  43781  ringcinvALTV  43805  islindeps  43988  snlindsntor  44006  blen1b  44129  nn0sumshdiglem1  44162  rrx2plordisom  44191  ehl2eudis0lt  44194  eenglngeehlnmlem2  44206  rrx2linest  44210  line2  44220  line2x  44222  line2y  44223  itschlc0xyqsol1  44234  itsclquadeu  44245