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  4464  elimhyp3v  4535  elimhyp4v  4536  keephyp3v  4541  ralsng  4620  opeqsng  5451  snopeqop  5454  frsn  5712  f1eq123d  6766  foeq123d  6767  f1oeq123d  6768  fnmptfvd  6987  fnotovb  7412  ofrfvalg  7632  eloprabi  8009  fnmpoovd  8030  suppsnop  8121  smoeq  8283  naddasslem1  8623  naddasslem2  8624  mapsnend  8976  infglbb  9398  wemapwe  9609  fseqenlem1  9937  dfac12lem2  10058  fin23lem22  10240  pwfseqlem5  10577  pwfseq  10578  enqbreq2  10834  lterpq  10884  ltdiv23  12038  lediv23  12039  negfi  12096  halfpos  12398  addltmul  12404  div4p1lem1div2  12423  supminf  12876  supxrbnd1  13264  supxrbnd2  13265  iccf1o  13440  fzshftral  13560  fzoshftral  13733  2tnp1ge0ge0  13779  dfceil2  13789  modirr  13895  hashen1  14323  seqcoll  14417  hash2prb  14425  hashle2prv  14431  hash3tpb  14448  s111  14569  swrdspsleq  14619  pfxnd0  14642  pfxeq  14649  wrd2ind  14676  2swrd2eqwrdeq  14906  eqwrds3  14914  limsupgle  15430  tanaddlem  16124  difmod0  16247  dvdssub  16264  addmodlteqALT  16285  dvdsmod  16289  oddp1even  16304  nn0o1gt2  16341  nn0oddm1d2  16345  bitscmp  16398  saddisjlem  16424  smueqlem  16450  ncoprmgcdne1b  16610  cncongr1  16627  cncongr2  16628  prmreclem5  16882  4sqlem11  16917  4sqlem17  16923  vdwmc2  16941  ismre  17543  acsfn  17616  dfiso2  17730  brcic  17756  isssc  17778  setcinv  18048  cat1  18055  intopsn  18613  sgrp1  18688  sgrppropd  18690  sgrp2nmndlem4  18890  nmzsubg  19131  eqg0subg  19162  conjnmzb  19219  gsmsymgreqlem2  19397  symgfixels  19400  f1omvdconj  19412  oddvdsnn0  19510  oddvds  19513  odcong  19515  odf1  19528  dpjeq  20027  pgpfac1lem2  20043  isomnd  20089  ogrpinvlt  20110  ring1  20282  rngcinv  20605  ringcinv  20639  lsmspsn  21071  lbsacsbs  21146  rngqiprngimf1lem  21284  lpigen  21325  prmirredlem  21462  znf1o  21541  znleval  21544  znunit  21553  islinds2  21803  islindf4  21828  psdmul  22142  scmatf1  22506  isclo  23062  maxlp  23122  1stccn  23438  xkoinjcn  23662  elmptrab  23802  fbunfip  23844  elfm  23922  fmid  23935  flfnei  23966  isflf  23968  isfcls  23984  fclsopn  23989  isfcf  24009  cnextfun  24039  eltsms  24108  prdsxmetlem  24343  elmopn  24417  metss  24483  comet  24488  elbl4  24538  metuel2  24540  nrmmetd  24549  metdsge  24825  tcphcph  25214  fmcfil  25249  cmscsscms  25350  rrxmet  25385  minveclem4  25409  shft2rab  25485  sca2rab  25489  volsup2  25582  mbfsup  25641  i1fmullem  25671  mbfi1fseqlem4  25695  xrge0f  25708  itg2monolem1  25727  ellimc2  25854  cnlimc  25865  mdegleb  26039  r1pid2  26137  facth1  26142  ulm2  26363  sineq0  26501  coseq1  26502  efeq1  26505  sinord  26511  root1eq1  26732  angrtmuld  26785  affineequiv3  26802  quad2  26816  dcubic  26823  cubic2  26825  dquartlem1  26828  dquart  26830  quart  26838  rlimcnp  26942  lgamucov  27015  mumullem2  27157  chtub  27189  fsumvma  27190  fsumvma2  27191  chpchtsum  27196  dchrelbas2  27214  bposlem7  27267  lgsneg  27298  lgsne0  27312  lgsprme0  27316  lgsqrlem2  27324  lgsquadlem1  27357  lgsquadlem2  27358  2lgs  27384  2lgsoddprm  27393  2sqreultb  27436  lrrecval2  27946  subscan1d  28109  n0lesm1lt  28373  bdaypw2bnd  28471  elreno2  28501  istrkg3ld  28543  tgcgr4  28613  iscgra1  28892  isleag  28929  iseqlg  28949  axcontlem7  29053  elntg2  29068  edg0iedg0  29138  ausgrusgrb  29248  usgr1v0edg  29340  nb3grprlem2  29464  uvtx01vtx  29480  cplgr3v  29518  vtxd0nedgb  29572  vtxdusgr0edgnelALT  29580  1egrvtxdg0  29595  upgr2wlk  29750  wlkp1lem8  29762  dfpth2  29812  wwlksnextbi  29977  s3wwlks2on  30039  sps3wwlks2on  30040  elwwlks2  30052  elwspths2spth  30053  rusgrnumwwlkl1  30054  clwwlkwwlksb  30139  0pth  30210  upgriseupth  30292  eupth2lem2  30304  eupth2lem3lem4  30316  eupth2lem3lem6  30318  nfrgr2v  30357  frgr3v  30360  fusgr2wsp2nb  30419  fusgreg2wsp  30421  extwwlkfab  30437  numclwwlk2lem1  30461  frgrreggt1  30478  imsmetlem  30776  ipz  30805  bnsscmcl  30954  minvecolem4  30966  hvsubcan  31160  hoeq2  31917  leoptri  32222  atcv0eq  32465  elimifd  32628  fdifsupp  32773  ressupprn  32778  gtiso  32789  2ndpreima  32796  fpwrelmapffslem  32820  quad3d  32837  xnn01gt  32858  fzsplit3  32881  fzo0opth  32891  islinds5  33442  grplsmid  33479  r1pid2OLD  33684  fldextrspunlsp  33834  constrsuc  33898  smatrcl  33956  rhmpreimacnlem  34044  pstmfval  34056  lmlim  34107  dya2ub  34430  eulerpartlemr  34534  isrrvv  34603  ballotlemsima  34676  signsvfn  34742  subfacp1lem3  35380  subfacp1lem5  35382  erdszelem1  35389  erdsze  35400  erdsze2lem2  35402  satf0op  35575  fmlafvel  35583  isfmlasuc  35586  filnetlem4  36579  bj-issetwt  37198  bj-sbceqgALT  37225  bj-raldifsn  37428  bj-idreseq  37492  bj-elid6  37500  bj-imdirval3  37514  bj-imdirco  37520  poimirlem24  37979  itg2addnclem2  38007  ftc1anclem1  38028  areacirclem1  38043  areacirclem5  38047  metf1o  38090  isass  38181  rngosn3  38259  brxrn  38718  lsatcv0eq  39507  cmtbr2N  39713  atlatmstc  39779  1cvrco  39932  cdleme3  40697  cdleme7  40709  cdlemg10c  41099  dvhopellsm  41577  dibord  41619  dib1dim2  41628  diblsmopel  41631  dihopelvalcpre  41708  dih1dimatlem  41789  hdmap14lem13  42340  hdmapoc  42391  cxp112d  42787  cxp111d  42788  elrfirn  43141  jm2.19lem2  43436  pwfi2f1o  43542  proot1ex  43642  isoeq145d  43864  sqrtcval  44086  brfvidRP  44133  uneqsn  44470  ntrclsfveq  44507  ntrclskb  44514  ntrclsk3  44515  ntrneiel2  44531  k0004lem3  44594  bcc0  44785  pwpwuni  45506  disjinfi  45640  rnmptbd2  45696  rnmptbd  45703  infxrbnd2  45816  ltmulneg  45839  ltdiv23neg  45841  rexabsle  45865  uzub  45877  supxrleubrnmptf  45897  supminfxr  45910  limsupre2lem  46170  limsupre2mpt  46176  limsupre3mpt  46180  limsupreuz  46183  limsuplt2  46199  liminflimsupclim  46253  xlimpnfxnegmnf  46260  liminfpnfuz  46262  xlimclim  46270  xlimbr  46273  xlimclim2lem  46285  xlimmnfmpt  46289  xlimpnfmpt  46290  fourierdlem113  46665  isvonmbl  47084  chnsubseqwl  47325  reuf1odnf  47567  addsubeq0  47756  ltnltne  47759  ceilbi  47797  iccpartgtl  47898  iccpartleu  47900  iccpartgel  47901  reuprpr  47995  fmtnoprmfac1  48040  fmtnoprmfac2  48042  quad1  48108  requad1  48110  requad2  48111  bits0ALTV  48167  bgoldbtbndlem1  48293  clnbgrel  48316  clnbupgrel  48322  dfsclnbgr6  48346  isubgredg  48354  gpgiedgdmel  48537  opgpgvtx  48543  gpg3kgrtriexlem5  48575  0nodd  48658  2nodd  48660  rngcinvALTV  48764  ringcinvALTV  48798  islindeps  48941  snlindsntor  48959  blen1b  49076  nn0sumshdiglem1  49109  0aryfvalel  49122  rrx2plordisom  49211  ehl2eudis0lt  49214  eenglngeehlnmlem2  49226  rrx2linest  49230  line2  49240  line2x  49242  line2y  49243  itschlc0xyqsol1  49254  itsclquadeu  49265  map0cor  49342  joindm2  49455  meetdm2  49457  islmd  50152  iscmd  50153