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  4478  elimhyp3v  4549  elimhyp4v  4550  keephyp3v  4555  ralsng  4634  opeqsng  5459  snopeqop  5462  frsn  5720  f1eq123d  6774  foeq123d  6775  f1oeq123d  6776  fnmptfvd  6995  fnotovb  7420  ofrfvalg  7640  eloprabi  8017  fnmpoovd  8039  suppsnop  8130  smoeq  8292  naddasslem1  8632  naddasslem2  8633  mapsnend  8985  infglbb  9407  wemapwe  9618  fseqenlem1  9946  dfac12lem2  10067  fin23lem22  10249  pwfseqlem5  10586  pwfseq  10587  enqbreq2  10843  lterpq  10893  ltdiv23  12045  lediv23  12046  negfi  12103  halfpos  12383  addltmul  12389  div4p1lem1div2  12408  supminf  12860  supxrbnd1  13248  supxrbnd2  13249  iccf1o  13424  fzshftral  13543  fzoshftral  13715  2tnp1ge0ge0  13761  dfceil2  13771  modirr  13877  hashen1  14305  seqcoll  14399  hash2prb  14407  hashle2prv  14413  hash3tpb  14430  s111  14551  swrdspsleq  14601  pfxnd0  14624  pfxeq  14631  wrd2ind  14658  2swrd2eqwrdeq  14888  eqwrds3  14896  limsupgle  15412  tanaddlem  16103  difmod0  16226  dvdssub  16243  addmodlteqALT  16264  dvdsmod  16268  oddp1even  16283  nn0o1gt2  16320  nn0oddm1d2  16324  bitscmp  16377  saddisjlem  16403  smueqlem  16429  ncoprmgcdne1b  16589  cncongr1  16606  cncongr2  16607  prmreclem5  16860  4sqlem11  16895  4sqlem17  16901  vdwmc2  16919  ismre  17521  acsfn  17594  dfiso2  17708  brcic  17734  isssc  17756  setcinv  18026  cat1  18033  intopsn  18591  sgrp1  18666  sgrppropd  18668  sgrp2nmndlem4  18865  nmzsubg  19106  eqg0subg  19137  conjnmzb  19194  gsmsymgreqlem2  19372  symgfixels  19375  f1omvdconj  19387  oddvdsnn0  19485  oddvds  19488  odcong  19490  odf1  19503  dpjeq  20002  pgpfac1lem2  20018  isomnd  20064  ogrpinvlt  20085  ring1  20257  rngcinv  20582  ringcinv  20616  lsmspsn  21048  lbsacsbs  21123  rngqiprngimf1lem  21261  lpigen  21302  prmirredlem  21439  znf1o  21518  znleval  21521  znunit  21530  islinds2  21780  islindf4  21805  psdmul  22121  scmatf1  22487  isclo  23043  maxlp  23103  1stccn  23419  xkoinjcn  23643  elmptrab  23783  fbunfip  23825  elfm  23903  fmid  23916  flfnei  23947  isflf  23949  isfcls  23965  fclsopn  23970  isfcf  23990  cnextfun  24020  eltsms  24089  prdsxmetlem  24324  elmopn  24398  metss  24464  comet  24469  elbl4  24519  metuel2  24521  nrmmetd  24530  metdsge  24806  tcphcph  25205  fmcfil  25240  cmscsscms  25341  rrxmet  25376  minveclem4  25400  shft2rab  25477  sca2rab  25481  volsup2  25574  mbfsup  25633  i1fmullem  25663  mbfi1fseqlem4  25687  xrge0f  25700  itg2monolem1  25719  ellimc2  25846  cnlimc  25857  mdegleb  26037  r1pid2  26135  facth1  26140  ulm2  26362  sineq0  26501  coseq1  26502  efeq1  26505  sinord  26511  root1eq1  26733  angrtmuld  26786  affineequiv3  26803  quad2  26817  dcubic  26824  cubic2  26826  dquartlem1  26829  dquart  26831  quart  26839  rlimcnp  26943  lgamucov  27016  mumullem2  27158  chtub  27191  fsumvma  27192  fsumvma2  27193  chpchtsum  27198  dchrelbas2  27216  bposlem7  27269  lgsneg  27300  lgsne0  27314  lgsprme0  27318  lgsqrlem2  27326  lgsquadlem1  27359  lgsquadlem2  27360  2lgs  27386  2lgsoddprm  27395  2sqreultb  27438  lrrecval2  27948  subscan1d  28111  n0lesm1lt  28375  bdaypw2bnd  28473  elreno2  28503  istrkg3ld  28545  tgcgr4  28615  iscgra1  28894  isleag  28931  iseqlg  28951  axcontlem7  29055  elntg2  29070  edg0iedg0  29140  ausgrusgrb  29250  usgr1v0edg  29342  nb3grprlem2  29466  uvtx01vtx  29482  cplgr3v  29520  vtxd0nedgb  29574  vtxdusgr0edgnelALT  29582  1egrvtxdg0  29597  upgr2wlk  29752  wlkp1lem8  29764  dfpth2  29814  wwlksnextbi  29979  s3wwlks2on  30041  sps3wwlks2on  30042  elwwlks2  30054  elwspths2spth  30055  rusgrnumwwlkl1  30056  clwwlkwwlksb  30141  0pth  30212  upgriseupth  30294  eupth2lem2  30306  eupth2lem3lem4  30318  eupth2lem3lem6  30320  nfrgr2v  30359  frgr3v  30362  fusgr2wsp2nb  30421  fusgreg2wsp  30423  extwwlkfab  30439  numclwwlk2lem1  30463  frgrreggt1  30480  imsmetlem  30778  ipz  30807  bnsscmcl  30956  minvecolem4  30968  hvsubcan  31162  hoeq2  31919  leoptri  32224  atcv0eq  32467  elimifd  32630  fdifsupp  32775  ressupprn  32780  gtiso  32791  2ndpreima  32798  fpwrelmapffslem  32822  quad3d  32840  xnn01gt  32861  fzsplit3  32884  fzo0opth  32894  islinds5  33460  grplsmid  33497  r1pid2OLD  33702  fldextrspunlsp  33852  constrsuc  33916  smatrcl  33974  rhmpreimacnlem  34062  pstmfval  34074  lmlim  34125  dya2ub  34448  eulerpartlemr  34552  isrrvv  34621  ballotlemsima  34694  signsvfn  34760  subfacp1lem3  35398  subfacp1lem5  35400  erdszelem1  35407  erdsze  35418  erdsze2lem2  35420  satf0op  35593  fmlafvel  35601  isfmlasuc  35604  filnetlem4  36597  bj-issetwt  37123  bj-sbceqgALT  37150  bj-raldifsn  37353  bj-idreseq  37417  bj-elid6  37425  bj-imdirval3  37439  bj-imdirco  37445  poimirlem24  37895  itg2addnclem2  37923  ftc1anclem1  37944  areacirclem1  37959  areacirclem5  37963  metf1o  38006  isass  38097  rngosn3  38175  brxrn  38634  lsatcv0eq  39423  cmtbr2N  39629  atlatmstc  39695  1cvrco  39848  cdleme3  40613  cdleme7  40625  cdlemg10c  41015  dvhopellsm  41493  dibord  41535  dib1dim2  41544  diblsmopel  41547  dihopelvalcpre  41624  dih1dimatlem  41705  hdmap14lem13  42256  hdmapoc  42307  cxp112d  42711  cxp111d  42712  elrfirn  43052  jm2.19lem2  43347  pwfi2f1o  43453  proot1ex  43553  isoeq145d  43775  sqrtcval  43997  brfvidRP  44044  uneqsn  44381  ntrclsfveq  44418  ntrclskb  44425  ntrclsk3  44426  ntrneiel2  44442  k0004lem3  44505  bcc0  44696  pwpwuni  45417  disjinfi  45551  rnmptbd2  45607  rnmptbd  45614  infxrbnd2  45727  ltmulneg  45750  ltdiv23neg  45752  rexabsle  45777  uzub  45789  supxrleubrnmptf  45809  supminfxr  45822  limsupre2lem  46082  limsupre2mpt  46088  limsupre3mpt  46092  limsupreuz  46095  limsuplt2  46111  liminflimsupclim  46165  xlimpnfxnegmnf  46172  liminfpnfuz  46174  xlimclim  46182  xlimbr  46185  xlimclim2lem  46197  xlimmnfmpt  46201  xlimpnfmpt  46202  fourierdlem113  46577  isvonmbl  46996  chnsubseqwl  47237  reuf1odnf  47467  addsubeq0  47656  ltnltne  47659  ceilbi  47693  iccpartgtl  47786  iccpartleu  47788  iccpartgel  47789  reuprpr  47883  fmtnoprmfac1  47925  fmtnoprmfac2  47927  quad1  47980  requad1  47982  requad2  47983  bits0ALTV  48039  bgoldbtbndlem1  48165  clnbgrel  48188  clnbupgrel  48194  dfsclnbgr6  48218  isubgredg  48226  gpgiedgdmel  48409  opgpgvtx  48415  gpg3kgrtriexlem5  48447  0nodd  48530  2nodd  48532  rngcinvALTV  48636  ringcinvALTV  48670  islindeps  48813  snlindsntor  48831  blen1b  48948  nn0sumshdiglem1  48981  0aryfvalel  48994  rrx2plordisom  49083  ehl2eudis0lt  49086  eenglngeehlnmlem2  49098  rrx2linest  49102  line2  49112  line2x  49114  line2y  49115  itschlc0xyqsol1  49126  itsclquadeu  49137  map0cor  49214  joindm2  49327  meetdm2  49329  islmd  50024  iscmd  50025