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  4481  elimhyp3v  4552  elimhyp4v  4553  keephyp3v  4558  ralsng  4635  opeqsng  5458  snopeqop  5461  frsn  5719  f1eq123d  6774  foeq123d  6775  f1oeq123d  6776  fnmptfvd  6995  fnotovb  7421  ofrfvalg  7641  eloprabi  8021  fnmpoovd  8043  suppsnop  8134  smoeq  8296  naddasslem1  8635  naddasslem2  8636  mapsnend  8984  infglbb  9419  wemapwe  9626  fseqenlem1  9953  dfac12lem2  10074  fin23lem22  10256  pwfseqlem5  10592  pwfseq  10593  enqbreq2  10849  lterpq  10899  ltdiv23  12050  lediv23  12051  negfi  12108  halfpos  12388  addltmul  12394  div4p1lem1div2  12413  supminf  12870  supxrbnd1  13257  supxrbnd2  13258  iccf1o  13433  fzshftral  13552  fzoshftral  13721  2tnp1ge0ge0  13767  dfceil2  13777  modirr  13883  hashen1  14311  seqcoll  14405  hash2prb  14413  hashle2prv  14419  hash3tpb  14436  s111  14556  swrdspsleq  14606  pfxnd0  14629  pfxeq  14637  wrd2ind  14664  2swrd2eqwrdeq  14895  eqwrds3  14903  limsupgle  15419  tanaddlem  16110  difmod0  16233  dvdssub  16250  addmodlteqALT  16271  dvdsmod  16275  oddp1even  16290  nn0o1gt2  16327  nn0oddm1d2  16331  bitscmp  16384  saddisjlem  16410  smueqlem  16436  ncoprmgcdne1b  16596  cncongr1  16613  cncongr2  16614  prmreclem5  16867  4sqlem11  16902  4sqlem17  16908  vdwmc2  16926  ismre  17527  acsfn  17596  dfiso2  17710  brcic  17736  isssc  17758  setcinv  18028  cat1  18035  intopsn  18557  sgrp1  18632  sgrppropd  18634  sgrp2nmndlem4  18831  nmzsubg  19073  eqg0subg  19104  conjnmzb  19161  gsmsymgreqlem2  19337  symgfixels  19340  f1omvdconj  19352  oddvdsnn0  19450  oddvds  19453  odcong  19455  odf1  19468  dpjeq  19967  pgpfac1lem2  19983  ring1  20195  rngcinv  20522  ringcinv  20556  lsmspsn  20967  lbsacsbs  21042  rngqiprngimf1lem  21180  lpigen  21221  prmirredlem  21358  znf1o  21437  znleval  21440  znunit  21449  islinds2  21698  islindf4  21723  psdmul  22029  scmatf1  22394  isclo  22950  maxlp  23010  1stccn  23326  xkoinjcn  23550  elmptrab  23690  fbunfip  23732  elfm  23810  fmid  23823  flfnei  23854  isflf  23856  isfcls  23872  fclsopn  23877  isfcf  23897  cnextfun  23927  eltsms  23996  prdsxmetlem  24232  elmopn  24306  metss  24372  comet  24377  elbl4  24427  metuel2  24429  nrmmetd  24438  metdsge  24714  tcphcph  25113  fmcfil  25148  cmscsscms  25249  rrxmet  25284  minveclem4  25308  shft2rab  25385  sca2rab  25389  volsup2  25482  mbfsup  25541  i1fmullem  25571  mbfi1fseqlem4  25595  xrge0f  25608  itg2monolem1  25627  ellimc2  25754  cnlimc  25765  mdegleb  25945  r1pid2  26043  facth1  26048  ulm2  26270  sineq0  26409  coseq1  26410  efeq1  26413  sinord  26419  root1eq1  26641  angrtmuld  26694  affineequiv3  26711  quad2  26725  dcubic  26732  cubic2  26734  dquartlem1  26737  dquart  26739  quart  26747  rlimcnp  26851  lgamucov  26924  mumullem2  27066  chtub  27099  fsumvma  27100  fsumvma2  27101  chpchtsum  27106  dchrelbas2  27124  bposlem7  27177  lgsneg  27208  lgsne0  27222  lgsprme0  27226  lgsqrlem2  27234  lgsquadlem1  27267  lgsquadlem2  27268  2lgs  27294  2lgsoddprm  27303  2sqreultb  27346  lrrecval2  27823  subscan1d  27982  n0slem1lt  28233  istrkg3ld  28364  tgcgr4  28434  iscgra1  28713  isleag  28750  iseqlg  28770  axcontlem7  28873  elntg2  28888  edg0iedg0  28958  ausgrusgrb  29068  usgr1v0edg  29160  nb3grprlem2  29284  uvtx01vtx  29300  cplgr3v  29338  vtxd0nedgb  29392  vtxdusgr0edgnelALT  29400  1egrvtxdg0  29415  upgr2wlk  29570  wlkp1lem8  29582  dfpth2  29632  wwlksnextbi  29797  s3wwlks2on  29859  elwwlks2  29869  elwspths2spth  29870  rusgrnumwwlkl1  29871  clwwlkwwlksb  29956  0pth  30027  upgriseupth  30109  eupth2lem2  30121  eupth2lem3lem4  30133  eupth2lem3lem6  30135  nfrgr2v  30174  frgr3v  30177  fusgr2wsp2nb  30236  fusgreg2wsp  30238  extwwlkfab  30254  numclwwlk2lem1  30278  frgrreggt1  30295  imsmetlem  30592  ipz  30621  bnsscmcl  30770  minvecolem4  30782  hvsubcan  30976  hoeq2  31733  leoptri  32038  atcv0eq  32281  elimifd  32445  fdifsupp  32581  ressupprn  32586  gtiso  32597  2ndpreima  32604  fpwrelmapffslem  32628  quad3d  32646  xnn01gt  32666  fzsplit3  32689  fzo0opth  32701  isomnd  32988  ogrpinvlt  33010  islinds5  33311  grplsmid  33348  r1pid2OLD  33547  fldextrspunlsp  33642  constrsuc  33701  smatrcl  33759  rhmpreimacnlem  33847  pstmfval  33859  lmlim  33910  dya2ub  34234  eulerpartlemr  34338  isrrvv  34407  ballotlemsima  34480  signsvfn  34546  subfacp1lem3  35142  subfacp1lem5  35144  erdszelem1  35151  erdsze  35162  erdsze2lem2  35164  satf0op  35337  fmlafvel  35345  isfmlasuc  35348  filnetlem4  36342  bj-issetwt  36836  bj-sbceqgALT  36863  bj-raldifsn  37061  bj-idreseq  37123  bj-elid6  37131  bj-imdirval3  37145  bj-imdirco  37151  poimirlem24  37611  itg2addnclem2  37639  ftc1anclem1  37660  areacirclem1  37675  areacirclem5  37679  metf1o  37722  isass  37813  rngosn3  37891  brxrn  38329  lsatcv0eq  39013  cmtbr2N  39219  atlatmstc  39285  1cvrco  39439  cdleme3  40204  cdleme7  40216  cdlemg10c  40606  dvhopellsm  41084  dibord  41126  dib1dim2  41135  diblsmopel  41138  dihopelvalcpre  41215  dih1dimatlem  41296  hdmap14lem13  41847  hdmapoc  41898  cxp112d  42302  cxp111d  42303  elrfirn  42656  jm2.19lem2  42952  pwfi2f1o  43058  proot1ex  43158  isoeq145d  43381  sqrtcval  43603  brfvidRP  43650  uneqsn  43987  ntrclsfveq  44024  ntrclskb  44031  ntrclsk3  44032  ntrneiel2  44048  k0004lem3  44111  bcc0  44302  pwpwuni  45024  disjinfi  45159  rnmptbd2  45216  rnmptbd  45223  infxrbnd2  45338  ltmulneg  45361  ltdiv23neg  45363  rexabsle  45388  uzub  45400  supxrleubrnmptf  45420  supminfxr  45433  limsupre2lem  45695  limsupre2mpt  45701  limsupre3mpt  45705  limsupreuz  45708  limsuplt2  45724  liminflimsupclim  45778  xlimpnfxnegmnf  45785  liminfpnfuz  45787  xlimclim  45795  xlimbr  45798  xlimclim2lem  45810  xlimmnfmpt  45814  xlimpnfmpt  45815  fourierdlem113  46190  isvonmbl  46609  reuf1odnf  47081  addsubeq0  47270  ltnltne  47273  ceilbi  47307  iccpartgtl  47400  iccpartleu  47402  iccpartgel  47403  reuprpr  47497  fmtnoprmfac1  47539  fmtnoprmfac2  47541  quad1  47594  requad1  47596  requad2  47597  bits0ALTV  47653  bgoldbtbndlem1  47779  clnbgrel  47802  clnbupgrel  47808  dfsclnbgr6  47831  isubgredg  47839  gpgiedgdmel  48013  opgpgvtx  48019  gpg3kgrtriexlem5  48051  0nodd  48131  2nodd  48133  rngcinvALTV  48237  ringcinvALTV  48271  islindeps  48415  snlindsntor  48433  blen1b  48550  nn0sumshdiglem1  48583  0aryfvalel  48596  rrx2plordisom  48685  ehl2eudis0lt  48688  eenglngeehlnmlem2  48700  rrx2linest  48704  line2  48714  line2x  48716  line2y  48717  itschlc0xyqsol1  48728  itsclquadeu  48739  map0cor  48816  joindm2  48929  meetdm2  48931  islmd  49627  iscmd  49628