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  4475  elimhyp3v  4546  elimhyp4v  4547  keephyp3v  4552  ralsng  4629  opeqsng  5450  snopeqop  5453  frsn  5711  f1eq123d  6760  foeq123d  6761  f1oeq123d  6762  fnmptfvd  6979  fnotovb  7405  ofrfvalg  7625  eloprabi  8005  fnmpoovd  8027  suppsnop  8118  smoeq  8280  naddasslem1  8619  naddasslem2  8620  mapsnend  8968  infglbb  9401  wemapwe  9612  fseqenlem1  9937  dfac12lem2  10058  fin23lem22  10240  pwfseqlem5  10576  pwfseq  10577  enqbreq2  10833  lterpq  10883  ltdiv23  12035  lediv23  12036  negfi  12093  halfpos  12373  addltmul  12379  div4p1lem1div2  12398  supminf  12855  supxrbnd1  13242  supxrbnd2  13243  iccf1o  13418  fzshftral  13537  fzoshftral  13706  2tnp1ge0ge0  13752  dfceil2  13762  modirr  13868  hashen1  14296  seqcoll  14390  hash2prb  14398  hashle2prv  14404  hash3tpb  14421  s111  14541  swrdspsleq  14591  pfxnd0  14614  pfxeq  14621  wrd2ind  14648  2swrd2eqwrdeq  14879  eqwrds3  14887  limsupgle  15403  tanaddlem  16094  difmod0  16217  dvdssub  16234  addmodlteqALT  16255  dvdsmod  16259  oddp1even  16274  nn0o1gt2  16311  nn0oddm1d2  16315  bitscmp  16368  saddisjlem  16394  smueqlem  16420  ncoprmgcdne1b  16580  cncongr1  16597  cncongr2  16598  prmreclem5  16851  4sqlem11  16886  4sqlem17  16892  vdwmc2  16910  ismre  17511  acsfn  17584  dfiso2  17698  brcic  17724  isssc  17746  setcinv  18016  cat1  18023  intopsn  18547  sgrp1  18622  sgrppropd  18624  sgrp2nmndlem4  18821  nmzsubg  19063  eqg0subg  19094  conjnmzb  19151  gsmsymgreqlem2  19329  symgfixels  19332  f1omvdconj  19344  oddvdsnn0  19442  oddvds  19445  odcong  19447  odf1  19460  dpjeq  19959  pgpfac1lem2  19975  isomnd  20021  ogrpinvlt  20042  ring1  20214  rngcinv  20541  ringcinv  20575  lsmspsn  21007  lbsacsbs  21082  rngqiprngimf1lem  21220  lpigen  21261  prmirredlem  21398  znf1o  21477  znleval  21480  znunit  21489  islinds2  21739  islindf4  21764  psdmul  22070  scmatf1  22435  isclo  22991  maxlp  23051  1stccn  23367  xkoinjcn  23591  elmptrab  23731  fbunfip  23773  elfm  23851  fmid  23864  flfnei  23895  isflf  23897  isfcls  23913  fclsopn  23918  isfcf  23938  cnextfun  23968  eltsms  24037  prdsxmetlem  24273  elmopn  24347  metss  24413  comet  24418  elbl4  24468  metuel2  24470  nrmmetd  24479  metdsge  24755  tcphcph  25154  fmcfil  25189  cmscsscms  25290  rrxmet  25325  minveclem4  25349  shft2rab  25426  sca2rab  25430  volsup2  25523  mbfsup  25582  i1fmullem  25612  mbfi1fseqlem4  25636  xrge0f  25649  itg2monolem1  25668  ellimc2  25795  cnlimc  25806  mdegleb  25986  r1pid2  26084  facth1  26089  ulm2  26311  sineq0  26450  coseq1  26451  efeq1  26454  sinord  26460  root1eq1  26682  angrtmuld  26735  affineequiv3  26752  quad2  26766  dcubic  26773  cubic2  26775  dquartlem1  26778  dquart  26780  quart  26788  rlimcnp  26892  lgamucov  26965  mumullem2  27107  chtub  27140  fsumvma  27141  fsumvma2  27142  chpchtsum  27147  dchrelbas2  27165  bposlem7  27218  lgsneg  27249  lgsne0  27263  lgsprme0  27267  lgsqrlem2  27275  lgsquadlem1  27308  lgsquadlem2  27309  2lgs  27335  2lgsoddprm  27344  2sqreultb  27387  lrrecval2  27871  subscan1d  28030  n0slem1lt  28281  istrkg3ld  28425  tgcgr4  28495  iscgra1  28774  isleag  28811  iseqlg  28831  axcontlem7  28934  elntg2  28949  edg0iedg0  29019  ausgrusgrb  29129  usgr1v0edg  29221  nb3grprlem2  29345  uvtx01vtx  29361  cplgr3v  29399  vtxd0nedgb  29453  vtxdusgr0edgnelALT  29461  1egrvtxdg0  29476  upgr2wlk  29631  wlkp1lem8  29643  dfpth2  29693  wwlksnextbi  29858  s3wwlks2on  29920  elwwlks2  29930  elwspths2spth  29931  rusgrnumwwlkl1  29932  clwwlkwwlksb  30017  0pth  30088  upgriseupth  30170  eupth2lem2  30182  eupth2lem3lem4  30194  eupth2lem3lem6  30196  nfrgr2v  30235  frgr3v  30238  fusgr2wsp2nb  30297  fusgreg2wsp  30299  extwwlkfab  30315  numclwwlk2lem1  30339  frgrreggt1  30356  imsmetlem  30653  ipz  30682  bnsscmcl  30831  minvecolem4  30843  hvsubcan  31037  hoeq2  31794  leoptri  32099  atcv0eq  32342  elimifd  32506  fdifsupp  32646  ressupprn  32651  gtiso  32662  2ndpreima  32669  fpwrelmapffslem  32694  quad3d  32712  xnn01gt  32732  fzsplit3  32755  fzo0opth  32767  islinds5  33323  grplsmid  33360  r1pid2OLD  33560  fldextrspunlsp  33660  constrsuc  33724  smatrcl  33782  rhmpreimacnlem  33870  pstmfval  33882  lmlim  33933  dya2ub  34257  eulerpartlemr  34361  isrrvv  34430  ballotlemsima  34503  signsvfn  34569  subfacp1lem3  35174  subfacp1lem5  35176  erdszelem1  35183  erdsze  35194  erdsze2lem2  35196  satf0op  35369  fmlafvel  35377  isfmlasuc  35380  filnetlem4  36374  bj-issetwt  36868  bj-sbceqgALT  36895  bj-raldifsn  37093  bj-idreseq  37155  bj-elid6  37163  bj-imdirval3  37177  bj-imdirco  37183  poimirlem24  37643  itg2addnclem2  37671  ftc1anclem1  37692  areacirclem1  37707  areacirclem5  37711  metf1o  37754  isass  37845  rngosn3  37923  brxrn  38361  lsatcv0eq  39045  cmtbr2N  39251  atlatmstc  39317  1cvrco  39471  cdleme3  40236  cdleme7  40248  cdlemg10c  40638  dvhopellsm  41116  dibord  41158  dib1dim2  41167  diblsmopel  41170  dihopelvalcpre  41247  dih1dimatlem  41328  hdmap14lem13  41879  hdmapoc  41930  cxp112d  42334  cxp111d  42335  elrfirn  42688  jm2.19lem2  42983  pwfi2f1o  43089  proot1ex  43189  isoeq145d  43412  sqrtcval  43634  brfvidRP  43681  uneqsn  44018  ntrclsfveq  44055  ntrclskb  44062  ntrclsk3  44063  ntrneiel2  44079  k0004lem3  44142  bcc0  44333  pwpwuni  45055  disjinfi  45190  rnmptbd2  45247  rnmptbd  45254  infxrbnd2  45368  ltmulneg  45391  ltdiv23neg  45393  rexabsle  45418  uzub  45430  supxrleubrnmptf  45450  supminfxr  45463  limsupre2lem  45725  limsupre2mpt  45731  limsupre3mpt  45735  limsupreuz  45738  limsuplt2  45754  liminflimsupclim  45808  xlimpnfxnegmnf  45815  liminfpnfuz  45817  xlimclim  45825  xlimbr  45828  xlimclim2lem  45840  xlimmnfmpt  45844  xlimpnfmpt  45845  fourierdlem113  46220  isvonmbl  46639  reuf1odnf  47111  addsubeq0  47300  ltnltne  47303  ceilbi  47337  iccpartgtl  47430  iccpartleu  47432  iccpartgel  47433  reuprpr  47527  fmtnoprmfac1  47569  fmtnoprmfac2  47571  quad1  47624  requad1  47626  requad2  47627  bits0ALTV  47683  bgoldbtbndlem1  47809  clnbgrel  47832  clnbupgrel  47838  dfsclnbgr6  47862  isubgredg  47870  gpgiedgdmel  48053  opgpgvtx  48059  gpg3kgrtriexlem5  48091  0nodd  48174  2nodd  48176  rngcinvALTV  48280  ringcinvALTV  48314  islindeps  48458  snlindsntor  48476  blen1b  48593  nn0sumshdiglem1  48626  0aryfvalel  48639  rrx2plordisom  48728  ehl2eudis0lt  48731  eenglngeehlnmlem2  48743  rrx2linest  48747  line2  48757  line2x  48759  line2y  48760  itschlc0xyqsol1  48771  itsclquadeu  48782  map0cor  48859  joindm2  48972  meetdm2  48974  islmd  49670  iscmd  49671