Theorem 3bitrd 308

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  2reu4lem  4478  elimhyp3v  4549  elimhyp4v  4550  keephyp3v  4555  ralsng  4632  opeqsng  5474  snopeqop  5477  frsn  5738  f1eq123d  6817  foeq123d  6818  f1oeq123d  6819  fnmptfvd  7041  fnotovb  7473  ofrfvalg  7702  eloprabi  8075  fnmpoovd  8099  suppsnop  8199  smoeq  8362  naddasslem1  8708  naddasslem2  8709  mapsnend  9068  infglbb  9488  wemapwe  9702  fseqenlem1  10107  dfac12lem2  10227  fin23lem22  10409  pwfseqlem5  10752  pwfseq  10753  enqbreq2  11009  lterpq  11059  ltdiv23  12212  lediv23  12213  negfi  12270  halfpos  12580  addltmul  12586  div4p1lem1div2  12605  supminf  13066  supxrbnd1  13455  supxrbnd2  13456  iccf1o  13631  fzshftral  13753  fzoshftral  13926  2tnp1ge0ge0  13973  dfceil2  13983  modirr  14089  hashen1  14518  seqcoll  14613  hash2prb  14621  hashle2prv  14627  hash3tpb  14644  s111  14768  swrdspsleq  14820  pfxnd0  14843  pfxeq  14850  wrd2ind  14877  2swrd2eqwrdeq  15112  eqwrds3  15120  limsupgle  15650  tanaddlem  16340  difmod0  16463  dvdssub  16480  addmodlteqALT  16501  dvdsmod  16505  oddp1even  16520  nn0o1gt2  16557  nn0oddm1d2  16561  bitscmp  16614  saddisjlem  16640  smueqlem  16666  ncoprmgcdne1b  16831  cncongr1  16848  cncongr2  16849  prmreclem5  17104  4sqlem11  17139  4sqlem17  17145  vdwmc2  17163  ismre  17766  acsfn  17839  dfiso2  17953  brcic  17979  isssc  18001  setcinv  18271  cat1  18278  intopsn  18838  sgrp1  18924  sgrppropd  18926  sgrp2nmndlem4  19133  nmzsubg  19381  eqg0subg  19417  conjnmzb  19473  gsmsymgreqlem2  19651  symgfixels  19654  f1omvdconj  19666  oddvdsnn0  19764  oddvds  19767  odcong  19769  odf1  19782  dpjeq  20281  pgpfac1lem2  20297  isomnd  20343  ogrpinvlt  20364  ring1  20547  rngcinv  20895  ringcinv  20929  lsmspsn  21365  lbsacsbs  21440  rngqiprngimf1lem  21596  lpigen  21665  prmirredlem  21784  znf1o  21863  znleval  21866  znunit  21875  islinds2  22125  islindf4  22150  psdmul  22493  scmatf1  22852  isclo  23411  maxlp  23471  1stccn  23788  xkoinjcn  24012  elmptrab  24152  fbunfip  24194  elfm  24272  fmid  24285  flfnei  24316  isflf  24318  isfcls  24334  fclsopn  24339  isfcf  24359  cnextfun  24389  eltsms  24458  prdsxmetlem  24693  elmopn  24767  metss  24833  comet  24838  elbl4  24888  metuel2  24890  nrmmetd  24899  metdsge  25175  tcphcph  25564  fmcfil  25599  cmscsscms  25700  rrxmet  25735  minveclem4  25759  shft2rab  25835  sca2rab  25839  volsup2  25932  mbfsup  25991  i1fmullem  26021  mbfi1fseqlem4  26045  xrge0f  26058  itg2monolem1  26077  ellimc2  26203  cnlimc  26214  mdegleb  26388  r1pid2  26486  facth1  26491  rnplynfin  26636  ulm2  26718  sineq0  26858  coseq1  26859  efeq1  26862  sinord  26868  root1eq1  27089  angrtmuld  27142  affineequiv3  27159  quad2  27173  dcubic  27180  cubic2  27182  dquartlem1  27185  dquart  27187  quart  27195  rlimcnp  27299  lgamucov  27371  mumullem2  27513  chtub  27545  fsumvma  27546  fsumvma2  27547  chpchtsum  27552  dchrelbas2  27570  bposlem7  27623  lgsneg  27654  lgsne0  27668  lgsprme0  27672  lgsqrlem2  27680  lgsquadlem1  27713  lgsquadlem2  27714  2lgs  27740  2lgsoddprm  27749  2sqreultb  27792  fltoprmgt3  28002  lrrecval2  28332  subscan1d  28495  n0lesm1lt  28759  bdaypw2bnd  28857  elreno2  28887  istrkg3ld  28929  tgcgr4  29000  iscgra1  29323  isleag  29372  iseqlg  29418  axcontlem7  29554  elntg2  29569  edg0iedg0  29639  ausgrusgrb  29752  usgr1v0edg  29844  nb3grprlem2  29968  uvtx01vtx  29984  cplgr3v  30022  vtxd0nedgb  30075  vtxdusgr0edgnelALT  30083  1egrvtxdg0  30098  upgr2wlk  30253  wlkp1lem8  30265  dfpth2  30320  wwlksnextbi  30489  s3wwlks2on  30551  sps3wwlks2on  30552  elwwlks2  30564  elwspths2spth  30565  rusgrnumwwlkl1  30566  clwwlkwwlksb  30651  0pth  30722  upgriseupth  30814  eupth2lem2  30826  eupth2lem3lem4  30838  eupth2lem3lem6  30840  nfrgr2v  30879  frgr3v  30882  fusgr2wsp2nb  30941  fusgreg2wsp  30943  extwwlkfab  30959  numclwwlk2lem1  30983  frgrreggt1  31000  imsmetlem  31298  ipz  31327  bnsscmcl  31476  minvecolem4  31488  hvsubcan  31682  hoeq2  32439  leoptri  32744  atcv0eq  32987  elimifd  33187  fdifsupp  33326  ressupprn  33331  gtiso  33342  2ndpreima  33349  fpwrelmapffslem  33371  quad3d  33388  xnn01gt  33409  fzsplit3  33432  fzo0opth  33442  rlocisunit  33884  islinds5  33970  grplsmid  34002  selvply1rhmlem2  34200  fldextrspunlsp  34353  constrsuc  34417  smatrcl  34475  rhmpreimacnlem  34563  pstmfval  34575  lmlim  34626  dya2ub  34949  eulerpartlemr  35053  isrrvv  35122  ballotlemsima  35195  signsvfn  35258  maxssj0  35946  subfacp1lem3  36034  subfacp1lem5  36036  erdszelem1  36043  erdsze  36054  erdsze2lem2  36056  satf0op  36229  fmlafvel  36237  isfmlasuc  36240  filnetlem4  37262  bj-issetwt  37880  bj-sbceqgALT  37907  bj-raldifsn  38114  bj-idreseq  38177  bj-elid6  38185  bj-imdirval3  38199  bj-imdirco  38205  poimirlem24  38656  itg2addnclem2  38684  ftc1anclem1  38705  areacirclem1  38720  areacirclem5  38724  metf1o  38783  isass  38874  rngosn3  38952  brxrn  39409  lsatcv0eq  40198  cmtbr2N  40404  atlatmstc  40470  1cvrco  40623  cdleme3  41388  cdleme7  41400  cdlemg10c  41790  dvhopellsm  42268  dibord  42310  dib1dim2  42319  diblsmopel  42322  dihopelvalcpre  42399  dih1dimatlem  42480  hdmap14lem13  43031  hdmapoc  43082  quadfac  43349  cxp112d  43486  cxp111d  43487  elrfirn  43800  jm2.19lem2  44091  pwfi2f1o  44192  proot1ex  44292  isoeq145d  44514  sqrtcval  44735  brfvidRP  44782  uneqsn  45119  ntrclsfveq  45156  ntrclskb  45163  ntrclsk3  45164  ntrneiel2  45180  k0004lem3  45243  bcc0  45418  pwpwuni  46168  disjinfi  46301  rnmptbd2  46355  rnmptbd  46362  infxrbnd2  46474  ltmulneg  46497  ltdiv23neg  46499  rexabsle  46523  uzub  46535  supxrleubrnmptf  46555  supminfxr  46568  limsupre2lem  46828  limsupre2mpt  46834  limsupre3mpt  46838  limsupreuz  46841  limsuplt2  46857  liminflimsupclim  46911  xlimpnfxnegmnf  46918  liminfpnfuz  46920  xlimclim  46928  xlimbr  46931  xlimclim2lem  46943  xlimmnfmpt  46947  xlimpnfmpt  46948  fourierdlem113  47323  isvonmbl  47742  chnsubseqwl  47983  reuf1odnf  48271  addsubeq0  48460  ltnltne  48463  ceilbi  48501  iccpartgtl  48602  iccpartleu  48604  iccpartgel  48605  reuprpr  48699  fmtnoprmfac1  48744  fmtnoprmfac2  48746  quad1  48812  requad1  48814  requad2  48815  bits0ALTV  48871  bgoldbtbndlem1  48997  clnbgrel  49020  clnbupgrel  49026  dfsclnbgr6  49050  isubgredg  49058  gpgiedgdmel  49241  opgpgvtx  49247  gpg3kgrtriexlem5  49279  0nodd  49361  2nodd  49363  rngcinvALTV  49467  ringcinvALTV  49501  crngprmringidom  49532  islindeps  49659  snlindsntor  49677  blen1b  49794  nn0sumshdiglem1  49827  0aryfvalel  49840  rrx2plordisom  49930  ehl2eudis0lt  49933  eenglngeehlnmlem2  49945  rrx2linest  49948  line2  49958  line2x  49960  line2y  49961  itschlc0xyqsol1  49972  itsclquadeu  49983  itscnhlinecirc02p  49991  map0cor  50060  joindm2  50176  meetdm2  50178  islmd  50942  iscmd  50943