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  3871  2reu4lem  4545  elimhyp3v  4615  elimhyp4v  4616  keephyp3v  4621  ralsng  4697  opeqsng  5522  snopeqop  5525  frsn  5787  f1eq123d  6854  foeq123d  6855  f1oeq123d  6856  fnmptfvd  7074  fnotovb  7500  ofrfvalg  7722  eloprabi  8104  fnmpoovd  8128  suppsnop  8219  smoeq  8406  naddasslem1  8750  naddasslem2  8751  mapsnend  9101  infglbb  9560  wemapwe  9766  fseqenlem1  10093  dfac12lem2  10214  fin23lem22  10396  pwfseqlem5  10732  pwfseq  10733  enqbreq2  10989  lterpq  11039  ltdiv23  12186  lediv23  12187  negfi  12244  halfpos  12523  addltmul  12529  div4p1lem1div2  12548  supminf  13000  supxrbnd1  13383  supxrbnd2  13384  iccf1o  13556  fzshftral  13672  fzoshftral  13834  2tnp1ge0ge0  13880  dfceil2  13890  modirr  13993  hashen1  14419  seqcoll  14513  hash2prb  14521  hashle2prv  14527  hash3tpb  14544  s111  14663  swrdspsleq  14713  pfxnd0  14736  pfxeq  14744  wrd2ind  14771  2swrd2eqwrdeq  15002  eqwrds3  15010  limsupgle  15523  tanaddlem  16214  dvdssub  16352  addmodlteqALT  16373  dvdsmod  16377  oddp1even  16392  nn0o1gt2  16429  nn0oddm1d2  16433  bitscmp  16484  saddisjlem  16510  smueqlem  16536  ncoprmgcdne1b  16697  cncongr1  16714  cncongr2  16715  prmreclem5  16967  4sqlem11  17002  4sqlem17  17008  vdwmc2  17026  ismre  17648  acsfn  17717  dfiso2  17833  brcic  17859  isssc  17881  setcinv  18157  cat1  18164  intopsn  18692  sgrp1  18767  sgrppropd  18769  sgrp2nmndlem4  18963  nmzsubg  19205  eqg0subg  19236  conjnmzb  19293  gsmsymgreqlem2  19473  symgfixels  19476  f1omvdconj  19488  oddvdsnn0  19586  oddvds  19589  odcong  19591  odf1  19604  dpjeq  20103  pgpfac1lem2  20119  ring1  20333  rngcinv  20659  ringcinv  20693  lsmspsn  21106  lbsacsbs  21181  rngqiprngimf1lem  21327  lpigen  21368  prmirredlem  21506  znf1o  21593  znleval  21596  znunit  21605  islinds2  21856  islindf4  21881  psdmul  22193  scmatf1  22558  isclo  23116  maxlp  23176  1stccn  23492  xkoinjcn  23716  elmptrab  23856  fbunfip  23898  elfm  23976  fmid  23989  flfnei  24020  isflf  24022  isfcls  24038  fclsopn  24043  isfcf  24063  cnextfun  24093  eltsms  24162  prdsxmetlem  24399  elmopn  24473  metss  24542  comet  24547  elbl4  24597  metuel2  24599  nrmmetd  24608  metdsge  24890  tcphcph  25290  fmcfil  25325  cmscsscms  25426  rrxmet  25461  minveclem4  25485  shft2rab  25562  sca2rab  25566  volsup2  25659  mbfsup  25718  i1fmullem  25748  mbfi1fseqlem4  25773  xrge0f  25786  itg2monolem1  25805  ellimc2  25932  cnlimc  25943  mdegleb  26123  r1pid2  26221  facth1  26226  ulm2  26446  sineq0  26584  coseq1  26585  efeq1  26588  sinord  26594  root1eq1  26816  angrtmuld  26869  affineequiv3  26886  quad2  26900  dcubic  26907  cubic2  26909  dquartlem1  26912  dquart  26914  quart  26922  rlimcnp  27026  lgamucov  27099  mumullem2  27241  chtub  27274  fsumvma  27275  fsumvma2  27276  chpchtsum  27281  dchrelbas2  27299  bposlem7  27352  lgsneg  27383  lgsne0  27397  lgsprme0  27401  lgsqrlem2  27409  lgsquadlem1  27442  lgsquadlem2  27443  2lgs  27469  2lgsoddprm  27478  2sqreultb  27521  lrrecval2  27991  istrkg3ld  28487  tgcgr4  28557  iscgra1  28836  isleag  28873  iseqlg  28893  axcontlem7  29003  elntg2  29018  edg0iedg0  29090  ausgrusgrb  29200  usgr1v0edg  29292  nb3grprlem2  29416  uvtx01vtx  29432  cplgr3v  29470  vtxd0nedgb  29524  vtxdusgr0edgnelALT  29532  1egrvtxdg0  29547  upgr2wlk  29704  wlkp1lem8  29716  wwlksnextbi  29927  s3wwlks2on  29989  elwwlks2  29999  elwspths2spth  30000  rusgrnumwwlkl1  30001  clwwlkwwlksb  30086  0pth  30157  upgriseupth  30239  eupth2lem2  30251  eupth2lem3lem4  30263  eupth2lem3lem6  30265  nfrgr2v  30304  frgr3v  30307  fusgr2wsp2nb  30366  fusgreg2wsp  30368  extwwlkfab  30384  numclwwlk2lem1  30408  frgrreggt1  30425  imsmetlem  30722  ipz  30751  bnsscmcl  30900  minvecolem4  30912  hvsubcan  31106  hoeq2  31863  leoptri  32168  atcv0eq  32411  elimifd  32566  ressupprn  32702  gtiso  32712  2ndpreima  32719  fpwrelmapffslem  32746  quad3d  32757  xnn01gt  32777  fzsplit3  32799  fzo0opth  32810  isomnd  33051  ogrpinvlt  33073  islinds5  33360  grplsmid  33397  r1pid2OLD  33594  constrsuc  33728  smatrcl  33742  rhmpreimacnlem  33830  pstmfval  33842  lmlim  33893  dya2ub  34235  eulerpartlemr  34339  isrrvv  34408  ballotlemsima  34480  signsvfn  34559  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem1  35159  erdsze  35170  erdsze2lem2  35172  satf0op  35345  fmlafvel  35353  isfmlasuc  35356  filnetlem4  36347  bj-issetwt  36841  bj-sbceqgALT  36868  bj-raldifsn  37066  bj-idreseq  37128  bj-elid6  37136  bj-imdirval3  37150  bj-imdirco  37156  poimirlem24  37604  itg2addnclem2  37632  ftc1anclem1  37653  areacirclem1  37668  areacirclem5  37672  metf1o  37715  isass  37806  rngosn3  37884  brxrn  38330  lsatcv0eq  39003  cmtbr2N  39209  atlatmstc  39275  1cvrco  39429  cdleme3  40194  cdleme7  40206  cdlemg10c  40596  dvhopellsm  41074  dibord  41116  dib1dim2  41125  diblsmopel  41128  dihopelvalcpre  41205  dih1dimatlem  41286  hdmap14lem13  41837  hdmapoc  41888  cxp112d  42329  cxp111d  42330  elrfirn  42651  jm2.19lem2  42947  pwfi2f1o  43053  proot1ex  43157  isoeq145d  43381  sqrtcval  43603  brfvidRP  43650  uneqsn  43987  ntrclsfveq  44024  ntrclskb  44031  ntrclsk3  44032  ntrneiel2  44048  k0004lem3  44111  bcc0  44309  pwpwuni  44959  disjinfi  45099  rnmptbd2  45158  rnmptbd  45165  infxrbnd2  45284  ltmulneg  45307  ltdiv23neg  45309  rexabsle  45334  uzub  45346  supxrleubrnmptf  45366  supminfxr  45379  limsupre2lem  45645  limsupre2mpt  45651  limsupre3mpt  45655  limsupreuz  45658  limsuplt2  45674  liminflimsupclim  45728  xlimpnfxnegmnf  45735  liminfpnfuz  45737  xlimclim  45745  xlimbr  45748  xlimclim2lem  45760  xlimmnfmpt  45764  xlimpnfmpt  45765  fourierdlem113  46140  isvonmbl  46559  reuf1odnf  47022  addsubeq0  47211  ltnltne  47214  iccpartgtl  47300  iccpartleu  47302  iccpartgel  47303  reuprpr  47397  fmtnoprmfac1  47439  fmtnoprmfac2  47441  quad1  47494  requad1  47496  requad2  47497  bits0ALTV  47553  bgoldbtbndlem1  47679  clnbgrel  47701  clnbupgrel  47707  dfsclnbgr6  47730  0nodd  47893  2nodd  47895  rngcinvALTV  47999  ringcinvALTV  48033  islindeps  48182  snlindsntor  48200  blen1b  48322  nn0sumshdiglem1  48355  0aryfvalel  48368  rrx2plordisom  48457  ehl2eudis0lt  48460  eenglngeehlnmlem2  48472  rrx2linest  48476  line2  48486  line2x  48488  line2y  48489  itschlc0xyqsol1  48500  itsclquadeu  48511  map0cor  48568  joindm2  48648  meetdm2  48650