Theorem 3bitrd 304

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 278	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 278	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  3779  2reu4lem  4453  elimhyp3v  4523  elimhyp4v  4524  keephyp3v  4529  ralsng  4606  opeqsng  5411  snopeqop  5414  frsn  5665  f1eq123d  6692  foeq123d  6693  f1oeq123d  6694  fnmptfvd  6900  fnotovb  7305  ofrfvalg  7519  eloprabi  7876  fnmpoovd  7898  suppsnop  7965  smoeq  8152  mapsnend  8780  infglbb  9180  wemapwe  9385  fseqenlem1  9711  dfac12lem2  9831  fin23lem22  10014  pwfseqlem5  10350  pwfseq  10351  enqbreq2  10607  lterpq  10657  ltdiv23  11796  lediv23  11797  negfi  11854  halfpos  12133  addltmul  12139  div4p1lem1div2  12158  supminf  12604  supxrbnd1  12984  supxrbnd2  12985  iccf1o  13157  fzshftral  13273  fzoshftral  13432  2tnp1ge0ge0  13477  dfceil2  13487  modirr  13590  hashen1  14013  seqcoll  14106  hash2prb  14114  hashle2prv  14120  s111  14248  swrdspsleq  14306  pfxnd0  14329  pfxeq  14337  wrd2ind  14364  2swrd2eqwrdeq  14594  eqwrds3  14604  limsupgle  15114  tanaddlem  15803  dvdssub  15941  addmodlteqALT  15962  dvdsmod  15966  oddp1even  15981  nn0o1gt2  16018  nn0oddm1d2  16022  bitscmp  16073  saddisjlem  16099  smueqlem  16125  ncoprmgcdne1b  16283  cncongr1  16300  cncongr2  16301  prmreclem5  16549  4sqlem11  16584  4sqlem17  16590  vdwmc2  16608  ismre  17216  acsfn  17285  dfiso2  17401  brcic  17427  isssc  17449  setcinv  17721  cat1  17728  intopsn  18253  sgrp1  18299  sgrp2nmndlem4  18482  nmzsubg  18708  conjnmzb  18784  gsmsymgreqlem2  18954  symgfixels  18957  f1omvdconj  18969  oddvdsnn0  19067  oddvds  19070  odcong  19072  odf1  19084  dpjeq  19577  pgpfac1lem2  19593  ring1  19756  lsmspsn  20261  lbsacsbs  20333  lpigen  20440  prmirredlem  20606  znf1o  20671  znleval  20674  znunit  20683  islinds2  20930  islindf4  20955  scmatf1  21588  isclo  22146  maxlp  22206  1stccn  22522  xkoinjcn  22746  elmptrab  22886  fbunfip  22928  elfm  23006  fmid  23019  flfnei  23050  isflf  23052  isfcls  23068  fclsopn  23073  isfcf  23093  cnextfun  23123  eltsms  23192  prdsxmetlem  23429  elmopn  23503  metss  23570  comet  23575  elbl4  23625  metuel2  23627  nrmmetd  23636  metdsge  23918  tcphcph  24306  fmcfil  24341  cmscsscms  24442  rrxmet  24477  minveclem4  24501  shft2rab  24577  sca2rab  24581  volsup2  24674  mbfsup  24733  i1fmullem  24763  mbfi1fseqlem4  24788  xrge0f  24801  itg2monolem1  24820  ellimc2  24946  cnlimc  24957  mdegleb  25134  facth1  25234  ulm2  25449  sineq0  25585  coseq1  25586  efeq1  25589  sinord  25595  root1eq1  25813  angrtmuld  25863  affineequiv3  25880  quad2  25894  dcubic  25901  cubic2  25903  dquartlem1  25906  dquart  25908  quart  25916  rlimcnp  26020  lgamucov  26092  mumullem2  26234  chtub  26265  fsumvma  26266  fsumvma2  26267  chpchtsum  26272  dchrelbas2  26290  bposlem7  26343  lgsneg  26374  lgsne0  26388  lgsprme0  26392  lgsqrlem2  26400  lgsquadlem1  26433  lgsquadlem2  26434  2lgs  26460  2lgsoddprm  26469  2sqreultb  26512  istrkg3ld  26726  tgcgr4  26796  iscgra1  27075  isleag  27112  iseqlg  27132  axcontlem7  27241  elntg2  27256  edg0iedg0  27328  ausgrusgrb  27438  usgr1v0edg  27527  nb3grprlem2  27651  uvtx01vtx  27667  cplgr3v  27705  vtxd0nedgb  27758  vtxdusgr0edgnelALT  27766  1egrvtxdg0  27781  upgr2wlk  27938  wlkp1lem8  27950  wwlksnextbi  28160  s3wwlks2on  28222  elwwlks2  28232  elwspths2spth  28233  rusgrnumwwlkl1  28234  clwwlkwwlksb  28319  0pth  28390  upgriseupth  28472  eupth2lem2  28484  eupth2lem3lem4  28496  eupth2lem3lem6  28498  nfrgr2v  28537  frgr3v  28540  fusgr2wsp2nb  28599  fusgreg2wsp  28601  extwwlkfab  28617  numclwwlk2lem1  28641  frgrreggt1  28658  imsmetlem  28953  ipz  28982  bnsscmcl  29131  minvecolem4  29143  hvsubcan  29337  hoeq2  30094  leoptri  30399  atcv0eq  30642  elimifd  30787  ressupprn  30926  gtiso  30935  2ndpreima  30942  fpwrelmapffslem  30969  xnn01gt  30995  fzsplit3  31017  isomnd  31229  ogrpinvlt  31251  islinds5  31465  grplsmid  31494  smatrcl  31648  rhmpreimacnlem  31736  pstmfval  31748  lmlim  31799  dya2ub  32137  eulerpartlemr  32241  isrrvv  32310  ballotlemsima  32382  signsvfn  32461  subfacp1lem3  33044  subfacp1lem5  33046  erdszelem1  33053  erdsze  33064  erdsze2lem2  33066  satf0op  33239  fmlafvel  33247  isfmlasuc  33250  lrrecval2  34024  filnetlem4  34497  bj-issetwt  34986  bj-sbceqgALT  35014  bj-raldifsn  35198  bj-idreseq  35260  bj-elid6  35268  bj-imdirval3  35282  bj-imdirco  35288  poimirlem24  35728  itg2addnclem2  35756  ftc1anclem1  35777  areacirclem1  35792  areacirclem5  35796  metf1o  35840  isass  35931  rngosn3  36009  brxrn  36431  lsatcv0eq  36988  cmtbr2N  37194  atlatmstc  37260  1cvrco  37413  cdleme3  38178  cdleme7  38190  cdlemg10c  38580  dvhopellsm  39058  dibord  39100  dib1dim2  39109  diblsmopel  39112  dihopelvalcpre  39189  dih1dimatlem  39270  hdmap14lem13  39821  hdmapoc  39872  elrfirn  40433  jm2.19lem2  40728  pwfi2f1o  40837  proot1ex  40942  sqrtcval  41138  brfvidRP  41185  uneqsn  41522  ntrclsfveq  41561  ntrclskb  41568  ntrclsk3  41569  ntrneiel2  41585  k0004lem3  41648  bcc0  41847  pwpwuni  42494  disjinfi  42620  rnmptbd2  42684  rnmptbd  42691  infxrbnd2  42798  ltmulneg  42822  ltdiv23neg  42824  rexabsle  42849  uzub  42861  supxrleubrnmptf  42881  supminfxr  42894  limsupre2lem  43155  limsupre2mpt  43161  limsupre3mpt  43165  limsupreuz  43168  limsuplt2  43184  liminflimsupclim  43238  xlimpnfxnegmnf  43245  liminfpnfuz  43247  xlimclim  43255  xlimbr  43258  xlimclim2lem  43270  xlimmnfmpt  43274  xlimpnfmpt  43275  fourierdlem113  43650  isvonmbl  44066  reuf1odnf  44486  addsubeq0  44676  ltnltne  44679  iccpartgtl  44766  iccpartleu  44768  iccpartgel  44769  reuprpr  44863  fmtnoprmfac1  44905  fmtnoprmfac2  44907  quad1  44960  requad1  44962  requad2  44963  bits0ALTV  45019  bgoldbtbndlem1  45145  0nodd  45252  2nodd  45254  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  islindeps  45682  snlindsntor  45700  blen1b  45822  nn0sumshdiglem1  45855  0aryfvalel  45868  rrx2plordisom  45957  ehl2eudis0lt  45960  eenglngeehlnmlem2  45972  rrx2linest  45976  line2  45986  line2x  45988  line2y  45989  itschlc0xyqsol1  46000  itsclquadeu  46011  map0cor  46070  joindm2  46150  meetdm2  46152