Theorem 3bitrd 307

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  2reu4lem  4474  elimhyp3v  4545  elimhyp4v  4546  keephyp3v  4551  ralsng  4631  opeqsng  5469  snopeqop  5472  frsn  5731  f1eq123d  6793  foeq123d  6794  f1oeq123d  6795  fnmptfvd  7017  fnotovb  7443  ofrfvalg  7663  eloprabi  8039  fnmpoovd  8060  suppsnop  8152  smoeq  8315  naddasslem1  8659  naddasslem2  8660  mapsnend  9011  infglbb  9432  wemapwe  9646  fseqenlem1  9974  dfac12lem2  10095  fin23lem22  10278  pwfseqlem5  10615  pwfseq  10616  enqbreq2  10872  lterpq  10922  ltdiv23  12077  lediv23  12078  negfi  12135  halfpos  12445  addltmul  12451  div4p1lem1div2  12470  supminf  12930  supxrbnd1  13318  supxrbnd2  13319  iccf1o  13494  fzshftral  13614  fzoshftral  13787  2tnp1ge0ge0  13833  dfceil2  13843  modirr  13949  hashen1  14377  seqcoll  14471  hash2prb  14479  hashle2prv  14485  hash3tpb  14502  s111  14623  swrdspsleq  14673  pfxnd0  14696  pfxeq  14703  wrd2ind  14730  2swrd2eqwrdeq  14960  eqwrds3  14968  limsupgle  15495  tanaddlem  16189  difmod0  16312  dvdssub  16329  addmodlteqALT  16350  dvdsmod  16354  oddp1even  16369  nn0o1gt2  16406  nn0oddm1d2  16410  bitscmp  16463  saddisjlem  16489  smueqlem  16515  ncoprmgcdne1b  16675  cncongr1  16692  cncongr2  16693  prmreclem5  16947  4sqlem11  16982  4sqlem17  16988  vdwmc2  17006  ismre  17609  acsfn  17682  dfiso2  17796  brcic  17822  isssc  17844  setcinv  18114  cat1  18121  intopsn  18679  sgrp1  18754  sgrppropd  18756  sgrp2nmndlem4  18956  nmzsubg  19197  eqg0subg  19228  conjnmzb  19284  gsmsymgreqlem2  19462  symgfixels  19465  f1omvdconj  19477  oddvdsnn0  19575  oddvds  19578  odcong  19580  odf1  19593  dpjeq  20092  pgpfac1lem2  20108  isomnd  20154  ogrpinvlt  20175  ring1  20347  rngcinv  20674  ringcinv  20708  lsmspsn  21139  lbsacsbs  21214  rngqiprngimf1lem  21352  lpigen  21393  prmirredlem  21512  znf1o  21591  znleval  21594  znunit  21603  islinds2  21853  islindf4  21878  psdmul  22219  scmatf1  22579  isclo  23135  maxlp  23195  1stccn  23511  xkoinjcn  23735  elmptrab  23875  fbunfip  23917  elfm  23995  fmid  24008  flfnei  24039  isflf  24041  isfcls  24057  fclsopn  24062  isfcf  24082  cnextfun  24112  eltsms  24181  prdsxmetlem  24416  elmopn  24490  metss  24556  comet  24561  elbl4  24611  metuel2  24613  nrmmetd  24622  metdsge  24898  tcphcph  25287  fmcfil  25322  cmscsscms  25423  rrxmet  25458  minveclem4  25482  shft2rab  25558  sca2rab  25562  volsup2  25655  mbfsup  25714  i1fmullem  25744  mbfi1fseqlem4  25768  xrge0f  25781  itg2monolem1  25800  ellimc2  25927  cnlimc  25938  mdegleb  26112  r1pid2  26210  facth1  26215  ulm2  26436  sineq0  26577  coseq1  26578  efeq1  26581  sinord  26587  root1eq1  26808  angrtmuld  26861  affineequiv3  26878  quad2  26892  dcubic  26899  cubic2  26901  dquartlem1  26904  dquart  26906  quart  26914  rlimcnp  27018  lgamucov  27090  mumullem2  27232  chtub  27264  fsumvma  27265  fsumvma2  27266  chpchtsum  27271  dchrelbas2  27289  bposlem7  27342  lgsneg  27373  lgsne0  27387  lgsprme0  27391  lgsqrlem2  27399  lgsquadlem1  27432  lgsquadlem2  27433  2lgs  27459  2lgsoddprm  27468  2sqreultb  27511  lrrecval2  28021  subscan1d  28184  n0lesm1lt  28448  bdaypw2bnd  28546  elreno2  28576  istrkg3ld  28618  tgcgr4  28688  iscgra1  28967  isleag  29004  iseqlg  29024  axcontlem7  29128  elntg2  29143  edg0iedg0  29213  ausgrusgrb  29323  usgr1v0edg  29415  nb3grprlem2  29539  uvtx01vtx  29555  cplgr3v  29593  vtxd0nedgb  29646  vtxdusgr0edgnelALT  29654  1egrvtxdg0  29669  upgr2wlk  29824  wlkp1lem8  29836  dfpth2  29886  wwlksnextbi  30051  s3wwlks2on  30113  sps3wwlks2on  30114  elwwlks2  30126  elwspths2spth  30127  rusgrnumwwlkl1  30128  clwwlkwwlksb  30213  0pth  30284  upgriseupth  30366  eupth2lem2  30378  eupth2lem3lem4  30390  eupth2lem3lem6  30392  nfrgr2v  30431  frgr3v  30434  fusgr2wsp2nb  30493  fusgreg2wsp  30495  extwwlkfab  30511  numclwwlk2lem1  30535  frgrreggt1  30552  imsmetlem  30850  ipz  30879  bnsscmcl  31028  minvecolem4  31040  hvsubcan  31234  hoeq2  31991  leoptri  32296  atcv0eq  32539  elimifd  32702  fdifsupp  32848  ressupprn  32853  gtiso  32864  2ndpreima  32871  fpwrelmapffslem  32895  quad3d  32912  xnn01gt  32933  fzsplit3  32956  fzo0opth  32966  rlocisunit  33418  islinds5  33514  grplsmid  33551  r1pid2OLD  33766  selvply1rhmlem2  33779  fldextrspunlsp  33932  constrsuc  33996  smatrcl  34054  rhmpreimacnlem  34142  pstmfval  34154  lmlim  34205  dya2ub  34528  eulerpartlemr  34632  isrrvv  34701  ballotlemsima  34774  signsvfn  34837  subfacp1lem3  35493  subfacp1lem5  35495  erdszelem1  35502  erdsze  35513  erdsze2lem2  35515  satf0op  35688  fmlafvel  35696  isfmlasuc  35699  filnetlem4  36702  bj-issetwt  37321  bj-sbceqgALT  37348  bj-raldifsn  37551  bj-idreseq  37615  bj-elid6  37623  bj-imdirval3  37637  bj-imdirco  37643  poimirlem24  38104  itg2addnclem2  38132  ftc1anclem1  38153  areacirclem1  38168  areacirclem5  38172  metf1o  38215  isass  38306  rngosn3  38384  brxrn  38843  lsatcv0eq  39632  cmtbr2N  39838  atlatmstc  39904  1cvrco  40057  cdleme3  40822  cdleme7  40834  cdlemg10c  41224  dvhopellsm  41702  dibord  41744  dib1dim2  41753  diblsmopel  41756  dihopelvalcpre  41833  dih1dimatlem  41914  hdmap14lem13  42465  hdmapoc  42516  cxp112d  42911  cxp111d  42912  elrfirn  43237  jm2.19lem2  43528  pwfi2f1o  43634  proot1ex  43734  isoeq145d  43956  sqrtcval  44178  brfvidRP  44225  uneqsn  44562  ntrclsfveq  44599  ntrclskb  44606  ntrclsk3  44607  ntrneiel2  44623  k0004lem3  44686  bcc0  44877  pwpwuni  45598  disjinfi  45731  rnmptbd2  45785  rnmptbd  45792  infxrbnd2  45905  ltmulneg  45928  ltdiv23neg  45930  rexabsle  45954  uzub  45966  supxrleubrnmptf  45986  supminfxr  45999  limsupre2lem  46259  limsupre2mpt  46265  limsupre3mpt  46269  limsupreuz  46272  limsuplt2  46288  liminflimsupclim  46342  xlimpnfxnegmnf  46349  liminfpnfuz  46351  xlimclim  46359  xlimbr  46362  xlimclim2lem  46374  xlimmnfmpt  46378  xlimpnfmpt  46379  fourierdlem113  46754  isvonmbl  47173  chnsubseqwl  47416  reuf1odnf  47662  addsubeq0  47851  ltnltne  47854  ceilbi  47892  iccpartgtl  47993  iccpartleu  47995  iccpartgel  47996  reuprpr  48090  fmtnoprmfac1  48135  fmtnoprmfac2  48137  quad1  48203  requad1  48205  requad2  48206  bits0ALTV  48262  bgoldbtbndlem1  48388  clnbgrel  48411  clnbupgrel  48417  dfsclnbgr6  48441  isubgredg  48449  gpgiedgdmel  48632  opgpgvtx  48638  gpg3kgrtriexlem5  48670  0nodd  48753  2nodd  48755  rngcinvALTV  48859  ringcinvALTV  48893  islindeps  49036  snlindsntor  49054  blen1b  49171  nn0sumshdiglem1  49204  0aryfvalel  49217  rrx2plordisom  49306  ehl2eudis0lt  49309  eenglngeehlnmlem2  49321  rrx2linest  49325  line2  49335  line2x  49337  line2y  49338  itschlc0xyqsol1  49349  itsclquadeu  49360  map0cor  49437  joindm2  49550  meetdm2  49552  islmd  50247  iscmd  50248