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:  sbceqalOLD  3857  2reu4lem  4527  elimhyp3v  4597  elimhyp4v  4598  keephyp3v  4603  ralsng  4679  opeqsng  5512  snopeqop  5515  frsn  5775  f1eq123d  6840  foeq123d  6841  f1oeq123d  6842  fnmptfvd  7060  fnotovb  7482  ofrfvalg  7704  eloprabi  8086  fnmpoovd  8110  suppsnop  8201  smoeq  8388  naddasslem1  8730  naddasslem2  8731  mapsnend  9074  infglbb  9528  wemapwe  9734  fseqenlem1  10061  dfac12lem2  10182  fin23lem22  10364  pwfseqlem5  10700  pwfseq  10701  enqbreq2  10957  lterpq  11007  ltdiv23  12156  lediv23  12157  negfi  12214  halfpos  12493  addltmul  12499  div4p1lem1div2  12518  supminf  12974  supxrbnd1  13359  supxrbnd2  13360  iccf1o  13532  fzshftral  13651  fzoshftral  13819  2tnp1ge0ge0  13865  dfceil2  13875  modirr  13979  hashen1  14405  seqcoll  14499  hash2prb  14507  hashle2prv  14513  hash3tpb  14530  s111  14649  swrdspsleq  14699  pfxnd0  14722  pfxeq  14730  wrd2ind  14757  2swrd2eqwrdeq  14988  eqwrds3  14996  limsupgle  15509  tanaddlem  16198  dvdssub  16337  addmodlteqALT  16358  dvdsmod  16362  oddp1even  16377  nn0o1gt2  16414  nn0oddm1d2  16418  bitscmp  16471  saddisjlem  16497  smueqlem  16523  ncoprmgcdne1b  16683  cncongr1  16700  cncongr2  16701  prmreclem5  16953  4sqlem11  16988  4sqlem17  16994  vdwmc2  17012  ismre  17634  acsfn  17703  dfiso2  17819  brcic  17845  isssc  17867  setcinv  18143  cat1  18150  intopsn  18679  sgrp1  18754  sgrppropd  18756  sgrp2nmndlem4  18953  nmzsubg  19195  eqg0subg  19226  conjnmzb  19283  gsmsymgreqlem2  19463  symgfixels  19466  f1omvdconj  19478  oddvdsnn0  19576  oddvds  19579  odcong  19581  odf1  19594  dpjeq  20093  pgpfac1lem2  20109  ring1  20323  rngcinv  20653  ringcinv  20687  lsmspsn  21100  lbsacsbs  21175  rngqiprngimf1lem  21321  lpigen  21362  prmirredlem  21500  znf1o  21587  znleval  21590  znunit  21599  islinds2  21850  islindf4  21875  psdmul  22187  scmatf1  22552  isclo  23110  maxlp  23170  1stccn  23486  xkoinjcn  23710  elmptrab  23850  fbunfip  23892  elfm  23970  fmid  23983  flfnei  24014  isflf  24016  isfcls  24032  fclsopn  24037  isfcf  24057  cnextfun  24087  eltsms  24156  prdsxmetlem  24393  elmopn  24467  metss  24536  comet  24541  elbl4  24591  metuel2  24593  nrmmetd  24602  metdsge  24884  tcphcph  25284  fmcfil  25319  cmscsscms  25420  rrxmet  25455  minveclem4  25479  shft2rab  25556  sca2rab  25560  volsup2  25653  mbfsup  25712  i1fmullem  25742  mbfi1fseqlem4  25767  xrge0f  25780  itg2monolem1  25799  ellimc2  25926  cnlimc  25937  mdegleb  26117  r1pid2  26215  facth1  26220  ulm2  26442  sineq0  26580  coseq1  26581  efeq1  26584  sinord  26590  root1eq1  26812  angrtmuld  26865  affineequiv3  26882  quad2  26896  dcubic  26903  cubic2  26905  dquartlem1  26908  dquart  26910  quart  26918  rlimcnp  27022  lgamucov  27095  mumullem2  27237  chtub  27270  fsumvma  27271  fsumvma2  27272  chpchtsum  27277  dchrelbas2  27295  bposlem7  27348  lgsneg  27379  lgsne0  27393  lgsprme0  27397  lgsqrlem2  27405  lgsquadlem1  27438  lgsquadlem2  27439  2lgs  27465  2lgsoddprm  27474  2sqreultb  27517  lrrecval2  27987  istrkg3ld  28483  tgcgr4  28553  iscgra1  28832  isleag  28869  iseqlg  28889  axcontlem7  28999  elntg2  29014  edg0iedg0  29086  ausgrusgrb  29196  usgr1v0edg  29288  nb3grprlem2  29412  uvtx01vtx  29428  cplgr3v  29466  vtxd0nedgb  29520  vtxdusgr0edgnelALT  29528  1egrvtxdg0  29543  upgr2wlk  29700  wlkp1lem8  29712  wwlksnextbi  29923  s3wwlks2on  29985  elwwlks2  29995  elwspths2spth  29996  rusgrnumwwlkl1  29997  clwwlkwwlksb  30082  0pth  30153  upgriseupth  30235  eupth2lem2  30247  eupth2lem3lem4  30259  eupth2lem3lem6  30261  nfrgr2v  30300  frgr3v  30303  fusgr2wsp2nb  30362  fusgreg2wsp  30364  extwwlkfab  30380  numclwwlk2lem1  30404  frgrreggt1  30421  imsmetlem  30718  ipz  30747  bnsscmcl  30896  minvecolem4  30908  hvsubcan  31102  hoeq2  31859  leoptri  32164  atcv0eq  32407  elimifd  32563  fdifsupp  32699  ressupprn  32704  gtiso  32715  2ndpreima  32722  fpwrelmapffslem  32749  quad3d  32760  xnn01gt  32780  fzsplit3  32801  fzo0opth  32812  isomnd  33060  ogrpinvlt  33082  islinds5  33374  grplsmid  33411  r1pid2OLD  33608  constrsuc  33742  smatrcl  33756  rhmpreimacnlem  33844  pstmfval  33856  lmlim  33907  dya2ub  34251  eulerpartlemr  34355  isrrvv  34424  ballotlemsima  34496  signsvfn  34575  subfacp1lem3  35166  subfacp1lem5  35168  erdszelem1  35175  erdsze  35186  erdsze2lem2  35188  satf0op  35361  fmlafvel  35369  isfmlasuc  35372  filnetlem4  36363  bj-issetwt  36857  bj-sbceqgALT  36884  bj-raldifsn  37082  bj-idreseq  37144  bj-elid6  37152  bj-imdirval3  37166  bj-imdirco  37172  poimirlem24  37630  itg2addnclem2  37658  ftc1anclem1  37679  areacirclem1  37694  areacirclem5  37698  metf1o  37741  isass  37832  rngosn3  37910  brxrn  38355  lsatcv0eq  39028  cmtbr2N  39234  atlatmstc  39300  1cvrco  39454  cdleme3  40219  cdleme7  40231  cdlemg10c  40621  dvhopellsm  41099  dibord  41141  dib1dim2  41150  diblsmopel  41153  dihopelvalcpre  41230  dih1dimatlem  41311  hdmap14lem13  41862  hdmapoc  41913  cxp112d  42355  cxp111d  42356  elrfirn  42682  jm2.19lem2  42978  pwfi2f1o  43084  proot1ex  43184  isoeq145d  43408  sqrtcval  43630  brfvidRP  43677  uneqsn  44014  ntrclsfveq  44051  ntrclskb  44058  ntrclsk3  44059  ntrneiel2  44075  k0004lem3  44138  bcc0  44335  pwpwuni  44996  disjinfi  45134  rnmptbd2  45193  rnmptbd  45200  infxrbnd2  45318  ltmulneg  45341  ltdiv23neg  45343  rexabsle  45368  uzub  45380  supxrleubrnmptf  45400  supminfxr  45413  limsupre2lem  45679  limsupre2mpt  45685  limsupre3mpt  45689  limsupreuz  45692  limsuplt2  45708  liminflimsupclim  45762  xlimpnfxnegmnf  45769  liminfpnfuz  45771  xlimclim  45779  xlimbr  45782  xlimclim2lem  45794  xlimmnfmpt  45798  xlimpnfmpt  45799  fourierdlem113  46174  isvonmbl  46593  reuf1odnf  47056  addsubeq0  47245  ltnltne  47248  iccpartgtl  47350  iccpartleu  47352  iccpartgel  47353  reuprpr  47447  fmtnoprmfac1  47489  fmtnoprmfac2  47491  quad1  47544  requad1  47546  requad2  47547  bits0ALTV  47603  bgoldbtbndlem1  47729  clnbgrel  47752  clnbupgrel  47758  dfsclnbgr6  47781  isubgredg  47789  0nodd  48013  2nodd  48015  rngcinvALTV  48119  ringcinvALTV  48153  islindeps  48298  snlindsntor  48316  blen1b  48437  nn0sumshdiglem1  48470  0aryfvalel  48483  rrx2plordisom  48572  ehl2eudis0lt  48575  eenglngeehlnmlem2  48587  rrx2linest  48591  line2  48601  line2x  48603  line2y  48604  itschlc0xyqsol1  48615  itsclquadeu  48626  map0cor  48684  joindm2  48764  meetdm2  48766