Theorem 3bitrd 308

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 282	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 282	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  2reu4lem  4479  elimhyp3v  4550  elimhyp4v  4551  keephyp3v  4556  ralsng  4636  opeqsng  5475  snopeqop  5478  frsn  5739  f1eq123d  6814  foeq123d  6815  f1oeq123d  6816  fnmptfvd  7038  fnotovb  7470  ofrfvalg  7699  eloprabi  8072  fnmpoovd  8096  suppsnop  8188  smoeq  8351  naddasslem1  8697  naddasslem2  8698  mapsnend  9057  infglbb  9477  wemapwe  9691  fseqenlem1  10096  dfac12lem2  10216  fin23lem22  10398  pwfseqlem5  10741  pwfseq  10742  enqbreq2  10998  lterpq  11048  ltdiv23  12201  lediv23  12202  negfi  12259  halfpos  12569  addltmul  12575  div4p1lem1div2  12594  supminf  13055  supxrbnd1  13444  supxrbnd2  13445  iccf1o  13620  fzshftral  13742  fzoshftral  13915  2tnp1ge0ge0  13962  dfceil2  13972  modirr  14078  hashen1  14507  seqcoll  14602  hash2prb  14610  hashle2prv  14616  hash3tpb  14633  s111  14756  swrdspsleq  14808  pfxnd0  14831  pfxeq  14838  wrd2ind  14865  2swrd2eqwrdeq  15099  eqwrds3  15107  limsupgle  15637  tanaddlem  16327  difmod0  16450  dvdssub  16467  addmodlteqALT  16488  dvdsmod  16492  oddp1even  16507  nn0o1gt2  16544  nn0oddm1d2  16548  bitscmp  16601  saddisjlem  16627  smueqlem  16653  ncoprmgcdne1b  16818  cncongr1  16835  cncongr2  16836  prmreclem5  17091  4sqlem11  17126  4sqlem17  17132  vdwmc2  17150  ismre  17753  acsfn  17826  dfiso2  17940  brcic  17966  isssc  17988  setcinv  18258  cat1  18265  intopsn  18825  sgrp1  18911  sgrppropd  18913  sgrp2nmndlem4  19120  nmzsubg  19368  eqg0subg  19404  conjnmzb  19460  gsmsymgreqlem2  19638  symgfixels  19641  f1omvdconj  19653  oddvdsnn0  19751  oddvds  19754  odcong  19756  odf1  19769  dpjeq  20268  pgpfac1lem2  20284  isomnd  20330  ogrpinvlt  20351  ring1  20534  rngcinv  20882  ringcinv  20916  lsmspsn  21352  lbsacsbs  21427  rngqiprngimf1lem  21583  lpigen  21652  prmirredlem  21771  znf1o  21850  znleval  21853  znunit  21862  islinds2  22112  islindf4  22137  psdmul  22480  scmatf1  22839  isclo  23398  maxlp  23458  1stccn  23775  xkoinjcn  23999  elmptrab  24139  fbunfip  24181  elfm  24259  fmid  24272  flfnei  24303  isflf  24305  isfcls  24321  fclsopn  24326  isfcf  24346  cnextfun  24376  eltsms  24445  prdsxmetlem  24680  elmopn  24754  metss  24820  comet  24825  elbl4  24875  metuel2  24877  nrmmetd  24886  metdsge  25162  tcphcph  25551  fmcfil  25586  cmscsscms  25687  rrxmet  25722  minveclem4  25746  shft2rab  25822  sca2rab  25826  volsup2  25919  mbfsup  25978  i1fmullem  26008  mbfi1fseqlem4  26032  xrge0f  26045  itg2monolem1  26064  ellimc2  26190  cnlimc  26201  mdegleb  26375  r1pid2  26473  facth1  26478  rnplynfin  26623  ulm2  26705  sineq0  26845  coseq1  26846  efeq1  26849  sinord  26855  root1eq1  27076  angrtmuld  27129  affineequiv3  27146  quad2  27160  dcubic  27167  cubic2  27169  dquartlem1  27172  dquart  27174  quart  27182  rlimcnp  27286  lgamucov  27358  mumullem2  27500  chtub  27532  fsumvma  27533  fsumvma2  27534  chpchtsum  27539  dchrelbas2  27557  bposlem7  27610  lgsneg  27641  lgsne0  27655  lgsprme0  27659  lgsqrlem2  27667  lgsquadlem1  27700  lgsquadlem2  27701  2lgs  27727  2lgsoddprm  27736  2sqreultb  27779  fltoprmgt3  27989  lrrecval2  28319  subscan1d  28482  n0lesm1lt  28746  bdaypw2bnd  28844  elreno2  28874  istrkg3ld  28916  tgcgr4  28987  iscgra1  29310  isleag  29359  iseqlg  29405  axcontlem7  29541  elntg2  29556  edg0iedg0  29626  ausgrusgrb  29739  usgr1v0edg  29831  nb3grprlem2  29955  uvtx01vtx  29971  cplgr3v  30009  vtxd0nedgb  30062  vtxdusgr0edgnelALT  30070  1egrvtxdg0  30085  upgr2wlk  30240  wlkp1lem8  30252  dfpth2  30307  wwlksnextbi  30476  s3wwlks2on  30538  sps3wwlks2on  30539  elwwlks2  30551  elwspths2spth  30552  rusgrnumwwlkl1  30553  clwwlkwwlksb  30638  0pth  30709  upgriseupth  30801  eupth2lem2  30813  eupth2lem3lem4  30825  eupth2lem3lem6  30827  nfrgr2v  30866  frgr3v  30869  fusgr2wsp2nb  30928  fusgreg2wsp  30930  extwwlkfab  30946  numclwwlk2lem1  30970  frgrreggt1  30987  imsmetlem  31285  ipz  31314  bnsscmcl  31463  minvecolem4  31475  hvsubcan  31669  hoeq2  32426  leoptri  32731  atcv0eq  32974  elimifd  33132  fdifsupp  33271  ressupprn  33276  gtiso  33287  2ndpreima  33294  fpwrelmapffslem  33317  quad3d  33334  xnn01gt  33355  fzsplit3  33378  fzo0opth  33388  rlocisunit  33830  islinds5  33916  grplsmid  33948  selvply1rhmlem2  34146  fldextrspunlsp  34299  constrsuc  34363  smatrcl  34421  rhmpreimacnlem  34509  pstmfval  34521  lmlim  34572  dya2ub  34895  eulerpartlemr  34999  isrrvv  35068  ballotlemsima  35141  signsvfn  35204  subfacp1lem3  35926  subfacp1lem5  35928  erdszelem1  35935  erdsze  35946  erdsze2lem2  35948  satf0op  36121  fmlafvel  36129  isfmlasuc  36132  filnetlem4  37149  bj-issetwt  37767  bj-sbceqgALT  37794  bj-raldifsn  38001  bj-idreseq  38063  bj-elid6  38071  bj-imdirval3  38085  bj-imdirco  38091  poimirlem24  38542  itg2addnclem2  38570  ftc1anclem1  38591  areacirclem1  38606  areacirclem5  38610  metf1o  38669  isass  38760  rngosn3  38838  brxrn  39295  lsatcv0eq  40084  cmtbr2N  40290  atlatmstc  40356  1cvrco  40509  cdleme3  41274  cdleme7  41286  cdlemg10c  41676  dvhopellsm  42154  dibord  42196  dib1dim2  42205  diblsmopel  42208  dihopelvalcpre  42285  dih1dimatlem  42366  hdmap14lem13  42917  hdmapoc  42968  quadfac  43235  cxp112d  43372  cxp111d  43373  elrfirn  43685  jm2.19lem2  43976  pwfi2f1o  44082  proot1ex  44182  isoeq145d  44404  sqrtcval  44626  brfvidRP  44673  uneqsn  45010  ntrclsfveq  45047  ntrclskb  45054  ntrclsk3  45055  ntrneiel2  45071  k0004lem3  45134  bcc0  45309  pwpwuni  46043  disjinfi  46176  rnmptbd2  46230  rnmptbd  46237  infxrbnd2  46349  ltmulneg  46372  ltdiv23neg  46374  rexabsle  46398  uzub  46410  supxrleubrnmptf  46430  supminfxr  46443  limsupre2lem  46703  limsupre2mpt  46709  limsupre3mpt  46713  limsupreuz  46716  limsuplt2  46732  liminflimsupclim  46786  xlimpnfxnegmnf  46793  liminfpnfuz  46795  xlimclim  46803  xlimbr  46806  xlimclim2lem  46818  xlimmnfmpt  46822  xlimpnfmpt  46823  fourierdlem113  47198  isvonmbl  47617  chnsubseqwl  47858  reuf1odnf  48146  addsubeq0  48335  ltnltne  48338  ceilbi  48376  iccpartgtl  48477  iccpartleu  48479  iccpartgel  48480  reuprpr  48574  fmtnoprmfac1  48619  fmtnoprmfac2  48621  quad1  48687  requad1  48689  requad2  48690  bits0ALTV  48746  bgoldbtbndlem1  48872  clnbgrel  48895  clnbupgrel  48901  dfsclnbgr6  48925  isubgredg  48933  gpgiedgdmel  49116  opgpgvtx  49122  gpg3kgrtriexlem5  49154  0nodd  49236  2nodd  49238  rngcinvALTV  49342  ringcinvALTV  49376  crngprmringidom  49407  islindeps  49534  snlindsntor  49552  blen1b  49669  nn0sumshdiglem1  49702  0aryfvalel  49715  rrx2plordisom  49804  ehl2eudis0lt  49807  eenglngeehlnmlem2  49819  rrx2linest  49823  line2  49833  line2x  49835  line2y  49836  itschlc0xyqsol1  49847  itsclquadeu  49858  map0cor  49934  joindm2  50045  meetdm2  50047  islmd  50742  iscmd  50743