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  4488  elimhyp3v  4559  elimhyp4v  4560  keephyp3v  4565  ralsng  4642  opeqsng  5466  snopeqop  5469  frsn  5729  f1eq123d  6795  foeq123d  6796  f1oeq123d  6797  fnmptfvd  7016  fnotovb  7442  ofrfvalg  7664  eloprabi  8045  fnmpoovd  8069  suppsnop  8160  smoeq  8322  naddasslem1  8661  naddasslem2  8662  mapsnend  9010  infglbb  9450  wemapwe  9657  fseqenlem1  9984  dfac12lem2  10105  fin23lem22  10287  pwfseqlem5  10623  pwfseq  10624  enqbreq2  10880  lterpq  10930  ltdiv23  12081  lediv23  12082  negfi  12139  halfpos  12419  addltmul  12425  div4p1lem1div2  12444  supminf  12901  supxrbnd1  13288  supxrbnd2  13289  iccf1o  13464  fzshftral  13583  fzoshftral  13752  2tnp1ge0ge0  13798  dfceil2  13808  modirr  13914  hashen1  14342  seqcoll  14436  hash2prb  14444  hashle2prv  14450  hash3tpb  14467  s111  14587  swrdspsleq  14637  pfxnd0  14660  pfxeq  14668  wrd2ind  14695  2swrd2eqwrdeq  14926  eqwrds3  14934  limsupgle  15450  tanaddlem  16141  difmod0  16264  dvdssub  16281  addmodlteqALT  16302  dvdsmod  16306  oddp1even  16321  nn0o1gt2  16358  nn0oddm1d2  16362  bitscmp  16415  saddisjlem  16441  smueqlem  16467  ncoprmgcdne1b  16627  cncongr1  16644  cncongr2  16645  prmreclem5  16898  4sqlem11  16933  4sqlem17  16939  vdwmc2  16957  ismre  17558  acsfn  17627  dfiso2  17741  brcic  17767  isssc  17789  setcinv  18059  cat1  18066  intopsn  18588  sgrp1  18663  sgrppropd  18665  sgrp2nmndlem4  18862  nmzsubg  19104  eqg0subg  19135  conjnmzb  19192  gsmsymgreqlem2  19368  symgfixels  19371  f1omvdconj  19383  oddvdsnn0  19481  oddvds  19484  odcong  19486  odf1  19499  dpjeq  19998  pgpfac1lem2  20014  ring1  20226  rngcinv  20553  ringcinv  20587  lsmspsn  20998  lbsacsbs  21073  rngqiprngimf1lem  21211  lpigen  21252  prmirredlem  21389  znf1o  21468  znleval  21471  znunit  21480  islinds2  21729  islindf4  21754  psdmul  22060  scmatf1  22425  isclo  22981  maxlp  23041  1stccn  23357  xkoinjcn  23581  elmptrab  23721  fbunfip  23763  elfm  23841  fmid  23854  flfnei  23885  isflf  23887  isfcls  23903  fclsopn  23908  isfcf  23928  cnextfun  23958  eltsms  24027  prdsxmetlem  24263  elmopn  24337  metss  24403  comet  24408  elbl4  24458  metuel2  24460  nrmmetd  24469  metdsge  24745  tcphcph  25144  fmcfil  25179  cmscsscms  25280  rrxmet  25315  minveclem4  25339  shft2rab  25416  sca2rab  25420  volsup2  25513  mbfsup  25572  i1fmullem  25602  mbfi1fseqlem4  25626  xrge0f  25639  itg2monolem1  25658  ellimc2  25785  cnlimc  25796  mdegleb  25976  r1pid2  26074  facth1  26079  ulm2  26301  sineq0  26440  coseq1  26441  efeq1  26444  sinord  26450  root1eq1  26672  angrtmuld  26725  affineequiv3  26742  quad2  26756  dcubic  26763  cubic2  26765  dquartlem1  26768  dquart  26770  quart  26778  rlimcnp  26882  lgamucov  26955  mumullem2  27097  chtub  27130  fsumvma  27131  fsumvma2  27132  chpchtsum  27137  dchrelbas2  27155  bposlem7  27208  lgsneg  27239  lgsne0  27253  lgsprme0  27257  lgsqrlem2  27265  lgsquadlem1  27298  lgsquadlem2  27299  2lgs  27325  2lgsoddprm  27334  2sqreultb  27377  lrrecval2  27854  subscan1d  28013  n0slem1lt  28264  istrkg3ld  28395  tgcgr4  28465  iscgra1  28744  isleag  28781  iseqlg  28801  axcontlem7  28904  elntg2  28919  edg0iedg0  28989  ausgrusgrb  29099  usgr1v0edg  29191  nb3grprlem2  29315  uvtx01vtx  29331  cplgr3v  29369  vtxd0nedgb  29423  vtxdusgr0edgnelALT  29431  1egrvtxdg0  29446  upgr2wlk  29603  wlkp1lem8  29615  dfpth2  29666  wwlksnextbi  29831  s3wwlks2on  29893  elwwlks2  29903  elwspths2spth  29904  rusgrnumwwlkl1  29905  clwwlkwwlksb  29990  0pth  30061  upgriseupth  30143  eupth2lem2  30155  eupth2lem3lem4  30167  eupth2lem3lem6  30169  nfrgr2v  30208  frgr3v  30211  fusgr2wsp2nb  30270  fusgreg2wsp  30272  extwwlkfab  30288  numclwwlk2lem1  30312  frgrreggt1  30329  imsmetlem  30626  ipz  30655  bnsscmcl  30804  minvecolem4  30816  hvsubcan  31010  hoeq2  31767  leoptri  32072  atcv0eq  32315  elimifd  32479  fdifsupp  32615  ressupprn  32620  gtiso  32631  2ndpreima  32638  fpwrelmapffslem  32662  quad3d  32680  xnn01gt  32700  fzsplit3  32723  fzo0opth  32735  isomnd  33022  ogrpinvlt  33044  islinds5  33345  grplsmid  33382  r1pid2OLD  33581  fldextrspunlsp  33676  constrsuc  33735  smatrcl  33793  rhmpreimacnlem  33881  pstmfval  33893  lmlim  33944  dya2ub  34268  eulerpartlemr  34372  isrrvv  34441  ballotlemsima  34514  signsvfn  34580  subfacp1lem3  35176  subfacp1lem5  35178  erdszelem1  35185  erdsze  35196  erdsze2lem2  35198  satf0op  35371  fmlafvel  35379  isfmlasuc  35382  filnetlem4  36376  bj-issetwt  36870  bj-sbceqgALT  36897  bj-raldifsn  37095  bj-idreseq  37157  bj-elid6  37165  bj-imdirval3  37179  bj-imdirco  37185  poimirlem24  37645  itg2addnclem2  37673  ftc1anclem1  37694  areacirclem1  37709  areacirclem5  37713  metf1o  37756  isass  37847  rngosn3  37925  brxrn  38363  lsatcv0eq  39047  cmtbr2N  39253  atlatmstc  39319  1cvrco  39473  cdleme3  40238  cdleme7  40250  cdlemg10c  40640  dvhopellsm  41118  dibord  41160  dib1dim2  41169  diblsmopel  41172  dihopelvalcpre  41249  dih1dimatlem  41330  hdmap14lem13  41881  hdmapoc  41932  cxp112d  42336  cxp111d  42337  elrfirn  42690  jm2.19lem2  42986  pwfi2f1o  43092  proot1ex  43192  isoeq145d  43415  sqrtcval  43637  brfvidRP  43684  uneqsn  44021  ntrclsfveq  44058  ntrclskb  44065  ntrclsk3  44066  ntrneiel2  44082  k0004lem3  44145  bcc0  44336  pwpwuni  45058  disjinfi  45193  rnmptbd2  45250  rnmptbd  45257  infxrbnd2  45372  ltmulneg  45395  ltdiv23neg  45397  rexabsle  45422  uzub  45434  supxrleubrnmptf  45454  supminfxr  45467  limsupre2lem  45729  limsupre2mpt  45735  limsupre3mpt  45739  limsupreuz  45742  limsuplt2  45758  liminflimsupclim  45812  xlimpnfxnegmnf  45819  liminfpnfuz  45821  xlimclim  45829  xlimbr  45832  xlimclim2lem  45844  xlimmnfmpt  45848  xlimpnfmpt  45849  fourierdlem113  46224  isvonmbl  46643  reuf1odnf  47112  addsubeq0  47301  ltnltne  47304  ceilbi  47338  iccpartgtl  47431  iccpartleu  47433  iccpartgel  47434  reuprpr  47528  fmtnoprmfac1  47570  fmtnoprmfac2  47572  quad1  47625  requad1  47627  requad2  47628  bits0ALTV  47684  bgoldbtbndlem1  47810  clnbgrel  47833  clnbupgrel  47839  dfsclnbgr6  47862  isubgredg  47870  gpgiedgdmel  48044  opgpgvtx  48050  gpg3kgrtriexlem5  48082  0nodd  48162  2nodd  48164  rngcinvALTV  48268  ringcinvALTV  48302  islindeps  48446  snlindsntor  48464  blen1b  48581  nn0sumshdiglem1  48614  0aryfvalel  48627  rrx2plordisom  48716  ehl2eudis0lt  48719  eenglngeehlnmlem2  48731  rrx2linest  48735  line2  48745  line2x  48747  line2y  48748  itschlc0xyqsol1  48759  itsclquadeu  48770  map0cor  48847  joindm2  48960  meetdm2  48962  islmd  49658  iscmd  49659