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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  sbceqalOLD  3784  2reu4lem  4457  elimhyp3v  4527  elimhyp4v  4528  keephyp3v  4533  ralsng  4610  opeqsng  5418  snopeqop  5421  frsn  5675  f1eq123d  6717  foeq123d  6718  f1oeq123d  6719  fnmptfvd  6927  fnotovb  7334  ofrfvalg  7550  eloprabi  7912  fnmpoovd  7936  suppsnop  8003  smoeq  8190  mapsnend  8835  infglbb  9259  wemapwe  9464  fseqenlem1  9789  dfac12lem2  9909  fin23lem22  10092  pwfseqlem5  10428  pwfseq  10429  enqbreq2  10685  lterpq  10735  ltdiv23  11875  lediv23  11876  negfi  11933  halfpos  12212  addltmul  12218  div4p1lem1div2  12237  supminf  12684  supxrbnd1  13064  supxrbnd2  13065  iccf1o  13237  fzshftral  13353  fzoshftral  13513  2tnp1ge0ge0  13558  dfceil2  13568  modirr  13671  hashen1  14094  seqcoll  14187  hash2prb  14195  hashle2prv  14201  s111  14329  swrdspsleq  14387  pfxnd0  14410  pfxeq  14418  wrd2ind  14445  2swrd2eqwrdeq  14675  eqwrds3  14685  limsupgle  15195  tanaddlem  15884  dvdssub  16022  addmodlteqALT  16043  dvdsmod  16047  oddp1even  16062  nn0o1gt2  16099  nn0oddm1d2  16103  bitscmp  16154  saddisjlem  16180  smueqlem  16206  ncoprmgcdne1b  16364  cncongr1  16381  cncongr2  16382  prmreclem5  16630  4sqlem11  16665  4sqlem17  16671  vdwmc2  16689  ismre  17308  acsfn  17377  dfiso2  17493  brcic  17519  isssc  17541  setcinv  17814  cat1  17821  intopsn  18347  sgrp1  18393  sgrp2nmndlem4  18576  nmzsubg  18802  conjnmzb  18878  gsmsymgreqlem2  19048  symgfixels  19051  f1omvdconj  19063  oddvdsnn0  19161  oddvds  19164  odcong  19166  odf1  19178  dpjeq  19671  pgpfac1lem2  19687  ring1  19850  lsmspsn  20355  lbsacsbs  20427  lpigen  20536  prmirredlem  20703  znf1o  20768  znleval  20771  znunit  20780  islinds2  21029  islindf4  21054  scmatf1  21689  isclo  22247  maxlp  22307  1stccn  22623  xkoinjcn  22847  elmptrab  22987  fbunfip  23029  elfm  23107  fmid  23120  flfnei  23151  isflf  23153  isfcls  23169  fclsopn  23174  isfcf  23194  cnextfun  23224  eltsms  23293  prdsxmetlem  23530  elmopn  23604  metss  23673  comet  23678  elbl4  23728  metuel2  23730  nrmmetd  23739  metdsge  24021  tcphcph  24410  fmcfil  24445  cmscsscms  24546  rrxmet  24581  minveclem4  24605  shft2rab  24681  sca2rab  24685  volsup2  24778  mbfsup  24837  i1fmullem  24867  mbfi1fseqlem4  24892  xrge0f  24905  itg2monolem1  24924  ellimc2  25050  cnlimc  25061  mdegleb  25238  facth1  25338  ulm2  25553  sineq0  25689  coseq1  25690  efeq1  25693  sinord  25699  root1eq1  25917  angrtmuld  25967  affineequiv3  25984  quad2  25998  dcubic  26005  cubic2  26007  dquartlem1  26010  dquart  26012  quart  26020  rlimcnp  26124  lgamucov  26196  mumullem2  26338  chtub  26369  fsumvma  26370  fsumvma2  26371  chpchtsum  26376  dchrelbas2  26394  bposlem7  26447  lgsneg  26478  lgsne0  26492  lgsprme0  26496  lgsqrlem2  26504  lgsquadlem1  26537  lgsquadlem2  26538  2lgs  26564  2lgsoddprm  26573  2sqreultb  26616  istrkg3ld  26831  tgcgr4  26901  iscgra1  27180  isleag  27217  iseqlg  27237  axcontlem7  27347  elntg2  27362  edg0iedg0  27434  ausgrusgrb  27544  usgr1v0edg  27633  nb3grprlem2  27757  uvtx01vtx  27773  cplgr3v  27811  vtxd0nedgb  27864  vtxdusgr0edgnelALT  27872  1egrvtxdg0  27887  upgr2wlk  28045  wlkp1lem8  28057  wwlksnextbi  28268  s3wwlks2on  28330  elwwlks2  28340  elwspths2spth  28341  rusgrnumwwlkl1  28342  clwwlkwwlksb  28427  0pth  28498  upgriseupth  28580  eupth2lem2  28592  eupth2lem3lem4  28604  eupth2lem3lem6  28606  nfrgr2v  28645  frgr3v  28648  fusgr2wsp2nb  28707  fusgreg2wsp  28709  extwwlkfab  28725  numclwwlk2lem1  28749  frgrreggt1  28766  imsmetlem  29061  ipz  29090  bnsscmcl  29239  minvecolem4  29251  hvsubcan  29445  hoeq2  30202  leoptri  30507  atcv0eq  30750  elimifd  30895  ressupprn  31033  gtiso  31042  2ndpreima  31049  fpwrelmapffslem  31076  xnn01gt  31102  fzsplit3  31124  isomnd  31336  ogrpinvlt  31358  islinds5  31572  grplsmid  31601  smatrcl  31755  rhmpreimacnlem  31843  pstmfval  31855  lmlim  31906  dya2ub  32246  eulerpartlemr  32350  isrrvv  32419  ballotlemsima  32491  signsvfn  32570  subfacp1lem3  33153  subfacp1lem5  33155  erdszelem1  33162  erdsze  33173  erdsze2lem2  33175  satf0op  33348  fmlafvel  33356  isfmlasuc  33359  lrrecval2  34106  filnetlem4  34579  bj-issetwt  35068  bj-sbceqgALT  35096  bj-raldifsn  35280  bj-idreseq  35342  bj-elid6  35350  bj-imdirval3  35364  bj-imdirco  35370  poimirlem24  35810  itg2addnclem2  35838  ftc1anclem1  35859  areacirclem1  35874  areacirclem5  35878  metf1o  35922  isass  36013  rngosn3  36091  brxrn  36511  lsatcv0eq  37068  cmtbr2N  37274  atlatmstc  37340  1cvrco  37493  cdleme3  38258  cdleme7  38270  cdlemg10c  38660  dvhopellsm  39138  dibord  39180  dib1dim2  39189  diblsmopel  39192  dihopelvalcpre  39269  dih1dimatlem  39350  hdmap14lem13  39901  hdmapoc  39952  elrfirn  40524  jm2.19lem2  40819  pwfi2f1o  40928  proot1ex  41033  sqrtcval  41256  brfvidRP  41303  uneqsn  41640  ntrclsfveq  41679  ntrclskb  41686  ntrclsk3  41687  ntrneiel2  41703  k0004lem3  41766  bcc0  41965  pwpwuni  42612  disjinfi  42738  rnmptbd2  42802  rnmptbd  42809  infxrbnd2  42915  ltmulneg  42939  ltdiv23neg  42941  rexabsle  42966  uzub  42978  supxrleubrnmptf  42998  supminfxr  43011  limsupre2lem  43272  limsupre2mpt  43278  limsupre3mpt  43282  limsupreuz  43285  limsuplt2  43301  liminflimsupclim  43355  xlimpnfxnegmnf  43362  liminfpnfuz  43364  xlimclim  43372  xlimbr  43375  xlimclim2lem  43387  xlimmnfmpt  43391  xlimpnfmpt  43392  fourierdlem113  43767  isvonmbl  44183  reuf1odnf  44610  addsubeq0  44799  ltnltne  44802  iccpartgtl  44889  iccpartleu  44891  iccpartgel  44892  reuprpr  44986  fmtnoprmfac1  45028  fmtnoprmfac2  45030  quad1  45083  requad1  45085  requad2  45086  bits0ALTV  45142  bgoldbtbndlem1  45268  0nodd  45375  2nodd  45377  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  ringcinvALTV  45625  islindeps  45805  snlindsntor  45823  blen1b  45945  nn0sumshdiglem1  45978  0aryfvalel  45991  rrx2plordisom  46080  ehl2eudis0lt  46083  eenglngeehlnmlem2  46095  rrx2linest  46099  line2  46109  line2x  46111  line2y  46112  itschlc0xyqsol1  46123  itsclquadeu  46134  map0cor  46193  joindm2  46273  meetdm2  46275