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 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  2reu4lem  4486  elimhyp3v  4557  elimhyp4v  4558  keephyp3v  4563  ralsng  4643  opeqsng  5484  snopeqop  5487  frsn  5747  f1eq123d  6810  foeq123d  6811  f1oeq123d  6812  fnmptfvd  7034  fnotovb  7460  ofrfvalg  7680  eloprabi  8056  fnmpoovd  8078  suppsnop  8170  smoeq  8333  naddasslem1  8677  naddasslem2  8678  mapsnend  9029  infglbb  9448  wemapwe  9662  fseqenlem1  10004  dfac12lem2  10124  fin23lem22  10307  pwfseqlem5  10644  pwfseq  10645  enqbreq2  10901  lterpq  10951  ltdiv23  12102  lediv23  12103  negfi  12160  halfpos  12470  addltmul  12476  div4p1lem1div2  12495  supminf  12955  supxrbnd1  13343  supxrbnd2  13344  iccf1o  13519  fzshftral  13639  fzoshftral  13812  2tnp1ge0ge0  13858  dfceil2  13868  modirr  13974  hashen1  14402  seqcoll  14497  hash2prb  14505  hashle2prv  14511  hash3tpb  14528  s111  14649  swrdspsleq  14699  pfxnd0  14722  pfxeq  14729  wrd2ind  14756  2swrd2eqwrdeq  14986  eqwrds3  14994  limsupgle  15524  tanaddlem  16218  difmod0  16341  dvdssub  16358  addmodlteqALT  16379  dvdsmod  16383  oddp1even  16398  nn0o1gt2  16435  nn0oddm1d2  16439  bitscmp  16492  saddisjlem  16518  smueqlem  16544  ncoprmgcdne1b  16704  cncongr1  16721  cncongr2  16722  prmreclem5  16976  4sqlem11  17011  4sqlem17  17017  vdwmc2  17035  ismre  17638  acsfn  17711  dfiso2  17825  brcic  17851  isssc  17873  setcinv  18143  cat1  18150  intopsn  18708  sgrp1  18783  sgrppropd  18785  sgrp2nmndlem4  18986  nmzsubg  19227  eqg0subg  19263  conjnmzb  19319  gsmsymgreqlem2  19497  symgfixels  19500  f1omvdconj  19512  oddvdsnn0  19610  oddvds  19613  odcong  19615  odf1  19628  dpjeq  20127  pgpfac1lem2  20143  isomnd  20189  ogrpinvlt  20210  ring1  20389  rngcinv  20718  ringcinv  20752  lsmspsn  21179  lbsacsbs  21254  rngqiprngimf1lem  21401  lpigen  21468  prmirredlem  21587  znf1o  21666  znleval  21669  znunit  21678  islinds2  21928  islindf4  21953  psdmul  22294  scmatf1  22653  isclo  23209  maxlp  23269  1stccn  23585  xkoinjcn  23809  elmptrab  23949  fbunfip  23991  elfm  24069  fmid  24082  flfnei  24113  isflf  24115  isfcls  24131  fclsopn  24136  isfcf  24156  cnextfun  24186  eltsms  24255  prdsxmetlem  24490  elmopn  24564  metss  24630  comet  24635  elbl4  24685  metuel2  24687  nrmmetd  24696  metdsge  24972  tcphcph  25361  fmcfil  25396  cmscsscms  25497  rrxmet  25532  minveclem4  25556  shft2rab  25632  sca2rab  25636  volsup2  25729  mbfsup  25788  i1fmullem  25818  mbfi1fseqlem4  25842  xrge0f  25855  itg2monolem1  25874  ellimc2  26001  cnlimc  26012  mdegleb  26186  r1pid2  26284  facth1  26289  ulm2  26510  sineq0  26651  coseq1  26652  efeq1  26655  sinord  26661  root1eq1  26882  angrtmuld  26935  affineequiv3  26952  quad2  26966  dcubic  26973  cubic2  26975  dquartlem1  26978  dquart  26980  quart  26988  rlimcnp  27092  lgamucov  27164  mumullem2  27306  chtub  27338  fsumvma  27339  fsumvma2  27340  chpchtsum  27345  dchrelbas2  27363  bposlem7  27416  lgsneg  27447  lgsne0  27461  lgsprme0  27465  lgsqrlem2  27473  lgsquadlem1  27506  lgsquadlem2  27507  2lgs  27533  2lgsoddprm  27542  2sqreultb  27585  lrrecval2  28095  subscan1d  28258  n0lesm1lt  28522  bdaypw2bnd  28620  elreno2  28650  istrkg3ld  28692  tgcgr4  28762  iscgra1  29074  isleag  29115  iseqlg  29135  axcontlem7  29257  elntg2  29272  edg0iedg0  29342  ausgrusgrb  29452  usgr1v0edg  29544  nb3grprlem2  29668  uvtx01vtx  29684  cplgr3v  29722  vtxd0nedgb  29775  vtxdusgr0edgnelALT  29783  1egrvtxdg0  29798  upgr2wlk  29953  wlkp1lem8  29965  dfpth2  30015  wwlksnextbi  30180  s3wwlks2on  30242  sps3wwlks2on  30243  elwwlks2  30255  elwspths2spth  30256  rusgrnumwwlkl1  30257  clwwlkwwlksb  30342  0pth  30413  upgriseupth  30495  eupth2lem2  30507  eupth2lem3lem4  30519  eupth2lem3lem6  30521  nfrgr2v  30560  frgr3v  30563  fusgr2wsp2nb  30622  fusgreg2wsp  30624  extwwlkfab  30640  numclwwlk2lem1  30664  frgrreggt1  30681  imsmetlem  30979  ipz  31008  bnsscmcl  31157  minvecolem4  31169  hvsubcan  31363  hoeq2  32120  leoptri  32425  atcv0eq  32668  elimifd  32826  fdifsupp  32967  ressupprn  32972  gtiso  32983  2ndpreima  32990  fpwrelmapffslem  33014  quad3d  33031  xnn01gt  33052  fzsplit3  33075  fzo0opth  33085  rlocisunit  33533  islinds5  33621  grplsmid  33653  selvply1rhmlem2  33852  fldextrspunlsp  34005  constrsuc  34069  smatrcl  34127  rhmpreimacnlem  34215  pstmfval  34227  lmlim  34278  dya2ub  34601  eulerpartlemr  34705  isrrvv  34774  ballotlemsima  34847  signsvfn  34910  subfacp1lem3  35569  subfacp1lem5  35571  erdszelem1  35578  erdsze  35589  erdsze2lem2  35591  satf0op  35764  fmlafvel  35772  isfmlasuc  35775  filnetlem4  36777  bj-issetwt  37395  bj-sbceqgALT  37422  bj-raldifsn  37625  bj-idreseq  37689  bj-elid6  37697  bj-imdirval3  37711  bj-imdirco  37717  poimirlem24  38178  itg2addnclem2  38206  ftc1anclem1  38227  areacirclem1  38242  areacirclem5  38246  metf1o  38289  isass  38380  rngosn3  38458  brxrn  38917  lsatcv0eq  39706  cmtbr2N  39912  atlatmstc  39978  1cvrco  40131  cdleme3  40896  cdleme7  40908  cdlemg10c  41298  dvhopellsm  41776  dibord  41818  dib1dim2  41827  diblsmopel  41830  dihopelvalcpre  41907  dih1dimatlem  41988  hdmap14lem13  42539  hdmapoc  42590  cxp112d  42985  cxp111d  42986  elrfirn  43311  jm2.19lem2  43602  pwfi2f1o  43708  proot1ex  43808  isoeq145d  44030  sqrtcval  44252  brfvidRP  44299  uneqsn  44636  ntrclsfveq  44673  ntrclskb  44680  ntrclsk3  44681  ntrneiel2  44697  k0004lem3  44760  bcc0  44935  pwpwuni  45662  disjinfi  45795  rnmptbd2  45849  rnmptbd  45856  infxrbnd2  45969  ltmulneg  45992  ltdiv23neg  45994  rexabsle  46018  uzub  46030  supxrleubrnmptf  46050  supminfxr  46063  limsupre2lem  46323  limsupre2mpt  46329  limsupre3mpt  46333  limsupreuz  46336  limsuplt2  46352  liminflimsupclim  46406  xlimpnfxnegmnf  46413  liminfpnfuz  46415  xlimclim  46423  xlimbr  46426  xlimclim2lem  46438  xlimmnfmpt  46442  xlimpnfmpt  46443  fourierdlem113  46818  isvonmbl  47237  chnsubseqwl  47480  reuf1odnf  47726  addsubeq0  47915  ltnltne  47918  ceilbi  47956  iccpartgtl  48057  iccpartleu  48059  iccpartgel  48060  reuprpr  48154  fmtnoprmfac1  48199  fmtnoprmfac2  48201  quad1  48267  requad1  48269  requad2  48270  bits0ALTV  48326  bgoldbtbndlem1  48452  clnbgrel  48475  clnbupgrel  48481  dfsclnbgr6  48505  isubgredg  48513  gpgiedgdmel  48696  opgpgvtx  48702  gpg3kgrtriexlem5  48734  0nodd  48817  2nodd  48819  rngcinvALTV  48923  ringcinvALTV  48957  crngprmringidom  48988  islindeps  49111  snlindsntor  49129  blen1b  49246  nn0sumshdiglem1  49279  0aryfvalel  49292  rrx2plordisom  49381  ehl2eudis0lt  49384  eenglngeehlnmlem2  49396  rrx2linest  49400  line2  49410  line2x  49412  line2y  49413  itschlc0xyqsol1  49424  itsclquadeu  49435  map0cor  49511  joindm2  49624  meetdm2  49626  islmd  50321  iscmd  50322