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  5763  f1eq123d  6825  foeq123d  6826  f1oeq123d  6827  fnmptfvd  7042  fnotovb  7462  ofrfvalg  7682  eloprabi  8053  fnmpoovd  8078  suppsnop  8168  smoeq  8356  naddasslem1  8699  naddasslem2  8700  mapsnend  9042  infglbb  9492  wemapwe  9698  fseqenlem1  10025  dfac12lem2  10145  fin23lem22  10328  pwfseqlem5  10664  pwfseq  10665  enqbreq2  10921  lterpq  10971  ltdiv23  12112  lediv23  12113  negfi  12170  halfpos  12449  addltmul  12455  div4p1lem1div2  12474  supminf  12926  supxrbnd1  13307  supxrbnd2  13308  iccf1o  13480  fzshftral  13596  fzoshftral  13756  2tnp1ge0ge0  13801  dfceil2  13811  modirr  13914  hashen1  14337  seqcoll  14432  hash2prb  14440  hashle2prv  14446  s111  14572  swrdspsleq  14622  pfxnd0  14645  pfxeq  14653  wrd2ind  14680  2swrd2eqwrdeq  14911  eqwrds3  14919  limsupgle  15428  tanaddlem  16116  dvdssub  16254  addmodlteqALT  16275  dvdsmod  16279  oddp1even  16294  nn0o1gt2  16331  nn0oddm1d2  16335  bitscmp  16386  saddisjlem  16412  smueqlem  16438  ncoprmgcdne1b  16594  cncongr1  16611  cncongr2  16612  prmreclem5  16860  4sqlem11  16895  4sqlem17  16901  vdwmc2  16919  ismre  17541  acsfn  17610  dfiso2  17726  brcic  17752  isssc  17774  setcinv  18050  cat1  18057  intopsn  18585  sgrp1  18660  sgrppropd  18662  sgrp2nmndlem4  18851  nmzsubg  19088  eqg0subg  19118  conjnmzb  19174  gsmsymgreqlem2  19347  symgfixels  19350  f1omvdconj  19362  oddvdsnn0  19460  oddvds  19463  odcong  19465  odf1  19478  dpjeq  19977  pgpfac1lem2  19993  ring1  20205  rngcinv  20529  ringcinv  20563  lsmspsn  20928  lbsacsbs  21003  df2idl2  21098  rngqiprngimf1lem  21142  lpigen  21183  prmirredlem  21332  znf1o  21417  znleval  21420  znunit  21429  islinds2  21678  islindf4  21703  scmatf1  22353  isclo  22911  maxlp  22971  1stccn  23287  xkoinjcn  23511  elmptrab  23651  fbunfip  23693  elfm  23771  fmid  23784  flfnei  23815  isflf  23817  isfcls  23833  fclsopn  23838  isfcf  23858  cnextfun  23888  eltsms  23957  prdsxmetlem  24194  elmopn  24268  metss  24337  comet  24342  elbl4  24392  metuel2  24394  nrmmetd  24403  metdsge  24685  tcphcph  25085  fmcfil  25120  cmscsscms  25221  rrxmet  25256  minveclem4  25280  shft2rab  25357  sca2rab  25361  volsup2  25454  mbfsup  25513  i1fmullem  25543  mbfi1fseqlem4  25568  xrge0f  25581  itg2monolem1  25600  ellimc2  25726  cnlimc  25737  mdegleb  25920  facth1  26020  ulm2  26236  sineq0  26373  coseq1  26374  efeq1  26377  sinord  26383  root1eq1  26604  angrtmuld  26654  affineequiv3  26671  quad2  26685  dcubic  26692  cubic2  26694  dquartlem1  26697  dquart  26699  quart  26707  rlimcnp  26811  lgamucov  26884  mumullem2  27026  chtub  27059  fsumvma  27060  fsumvma2  27061  chpchtsum  27066  dchrelbas2  27084  bposlem7  27137  lgsneg  27168  lgsne0  27182  lgsprme0  27186  lgsqrlem2  27194  lgsquadlem1  27227  lgsquadlem2  27228  2lgs  27254  2lgsoddprm  27263  2sqreultb  27306  lrrecval2  27771  istrkg3ld  28146  tgcgr4  28216  iscgra1  28495  isleag  28532  iseqlg  28552  axcontlem7  28662  elntg2  28677  edg0iedg0  28749  ausgrusgrb  28859  usgr1v0edg  28948  nb3grprlem2  29072  uvtx01vtx  29088  cplgr3v  29126  vtxd0nedgb  29179  vtxdusgr0edgnelALT  29187  1egrvtxdg0  29202  upgr2wlk  29359  wlkp1lem8  29371  wwlksnextbi  29582  s3wwlks2on  29644  elwwlks2  29654  elwspths2spth  29655  rusgrnumwwlkl1  29656  clwwlkwwlksb  29741  0pth  29812  upgriseupth  29894  eupth2lem2  29906  eupth2lem3lem4  29918  eupth2lem3lem6  29920  nfrgr2v  29959  frgr3v  29962  fusgr2wsp2nb  30021  fusgreg2wsp  30023  extwwlkfab  30039  numclwwlk2lem1  30063  frgrreggt1  30080  imsmetlem  30377  ipz  30406  bnsscmcl  30555  minvecolem4  30567  hvsubcan  30761  hoeq2  31518  leoptri  31823  atcv0eq  32066  elimifd  32209  ressupprn  32346  gtiso  32356  2ndpreima  32363  fpwrelmapffslem  32391  xnn01gt  32417  fzsplit3  32439  isomnd  32656  ogrpinvlt  32678  islinds5  32921  grplsmid  32955  r1pid2  33121  smatrcl  33241  rhmpreimacnlem  33329  pstmfval  33341  lmlim  33392  dya2ub  33734  eulerpartlemr  33838  isrrvv  33907  ballotlemsima  33979  signsvfn  34058  subfacp1lem3  34638  subfacp1lem5  34640  erdszelem1  34647  erdsze  34658  erdsze2lem2  34660  satf0op  34833  fmlafvel  34841  isfmlasuc  34844  filnetlem4  35732  bj-issetwt  36220  bj-sbceqgALT  36248  bj-raldifsn  36447  bj-idreseq  36509  bj-elid6  36517  bj-imdirval3  36531  bj-imdirco  36537  poimirlem24  36978  itg2addnclem2  37006  ftc1anclem1  37027  areacirclem1  37042  areacirclem5  37046  metf1o  37089  isass  37180  rngosn3  37258  brxrn  37710  lsatcv0eq  38383  cmtbr2N  38589  atlatmstc  38655  1cvrco  38809  cdleme3  39574  cdleme7  39586  cdlemg10c  39976  dvhopellsm  40454  dibord  40496  dib1dim2  40505  diblsmopel  40508  dihopelvalcpre  40585  dih1dimatlem  40666  hdmap14lem13  41217  hdmapoc  41268  elrfirn  41898  jm2.19lem2  42194  pwfi2f1o  42303  proot1ex  42408  isoeq145d  42635  sqrtcval  42857  brfvidRP  42904  uneqsn  43241  ntrclsfveq  43278  ntrclskb  43285  ntrclsk3  43286  ntrneiel2  43302  k0004lem3  43365  bcc0  43564  pwpwuni  44208  disjinfi  44352  rnmptbd2  44414  rnmptbd  44421  infxrbnd2  44540  ltmulneg  44563  ltdiv23neg  44565  rexabsle  44590  uzub  44602  supxrleubrnmptf  44622  supminfxr  44635  limsupre2lem  44901  limsupre2mpt  44907  limsupre3mpt  44911  limsupreuz  44914  limsuplt2  44930  liminflimsupclim  44984  xlimpnfxnegmnf  44991  liminfpnfuz  44993  xlimclim  45001  xlimbr  45004  xlimclim2lem  45016  xlimmnfmpt  45020  xlimpnfmpt  45021  fourierdlem113  45396  isvonmbl  45815  reuf1odnf  46276  addsubeq0  46465  ltnltne  46468  iccpartgtl  46555  iccpartleu  46557  iccpartgel  46558  reuprpr  46652  fmtnoprmfac1  46694  fmtnoprmfac2  46696  quad1  46749  requad1  46751  requad2  46752  bits0ALTV  46808  bgoldbtbndlem1  46934  0nodd  47009  2nodd  47011  rngcinvALTV  47115  ringcinvALTV  47149  islindeps  47298  snlindsntor  47316  blen1b  47438  nn0sumshdiglem1  47471  0aryfvalel  47484  rrx2plordisom  47573  ehl2eudis0lt  47576  eenglngeehlnmlem2  47588  rrx2linest  47592  line2  47602  line2x  47604  line2y  47605  itschlc0xyqsol1  47616  itsclquadeu  47627  map0cor  47685  joindm2  47765  meetdm2  47767