Theorem 3bitrd 304

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  3804  2reu4lem  4481  elimhyp3v  4551  elimhyp4v  4552  keephyp3v  4557  ralsng  4632  opeqsng  5458  snopeqop  5461  frsn  5717  f1eq123d  6773  foeq123d  6774  f1oeq123d  6775  fnmptfvd  6988  fnotovb  7401  ofrfvalg  7617  eloprabi  7987  fnmpoovd  8011  suppsnop  8101  smoeq  8288  mapsnend  8938  infglbb  9385  wemapwe  9591  fseqenlem1  9918  dfac12lem2  10038  fin23lem22  10221  pwfseqlem5  10557  pwfseq  10558  enqbreq2  10814  lterpq  10864  ltdiv23  12004  lediv23  12005  negfi  12062  halfpos  12341  addltmul  12347  div4p1lem1div2  12366  supminf  12814  supxrbnd1  13194  supxrbnd2  13195  iccf1o  13367  fzshftral  13483  fzoshftral  13643  2tnp1ge0ge0  13688  dfceil2  13698  modirr  13801  hashen1  14224  seqcoll  14317  hash2prb  14325  hashle2prv  14331  s111  14457  swrdspsleq  14511  pfxnd0  14534  pfxeq  14542  wrd2ind  14569  2swrd2eqwrdeq  14800  eqwrds3  14810  limsupgle  15319  tanaddlem  16008  dvdssub  16146  addmodlteqALT  16167  dvdsmod  16171  oddp1even  16186  nn0o1gt2  16223  nn0oddm1d2  16227  bitscmp  16278  saddisjlem  16304  smueqlem  16330  ncoprmgcdne1b  16486  cncongr1  16503  cncongr2  16504  prmreclem5  16752  4sqlem11  16787  4sqlem17  16793  vdwmc2  16811  ismre  17430  acsfn  17499  dfiso2  17615  brcic  17641  isssc  17663  setcinv  17936  cat1  17943  intopsn  18469  sgrp1  18515  sgrp2nmndlem4  18698  nmzsubg  18926  conjnmzb  19002  gsmsymgreqlem2  19172  symgfixels  19175  f1omvdconj  19187  oddvdsnn0  19285  oddvds  19288  odcong  19290  odf1  19303  dpjeq  19797  pgpfac1lem2  19813  ring1  19979  lsmspsn  20498  lbsacsbs  20570  lpigen  20679  prmirredlem  20846  znf1o  20911  znleval  20914  znunit  20923  islinds2  21172  islindf4  21197  scmatf1  21832  isclo  22390  maxlp  22450  1stccn  22766  xkoinjcn  22990  elmptrab  23130  fbunfip  23172  elfm  23250  fmid  23263  flfnei  23294  isflf  23296  isfcls  23312  fclsopn  23317  isfcf  23337  cnextfun  23367  eltsms  23436  prdsxmetlem  23673  elmopn  23747  metss  23816  comet  23821  elbl4  23871  metuel2  23873  nrmmetd  23882  metdsge  24164  tcphcph  24553  fmcfil  24588  cmscsscms  24689  rrxmet  24724  minveclem4  24748  shft2rab  24824  sca2rab  24828  volsup2  24921  mbfsup  24980  i1fmullem  25010  mbfi1fseqlem4  25035  xrge0f  25048  itg2monolem1  25067  ellimc2  25193  cnlimc  25204  mdegleb  25381  facth1  25481  ulm2  25696  sineq0  25832  coseq1  25833  efeq1  25836  sinord  25842  root1eq1  26060  angrtmuld  26110  affineequiv3  26127  quad2  26141  dcubic  26148  cubic2  26150  dquartlem1  26153  dquart  26155  quart  26163  rlimcnp  26267  lgamucov  26339  mumullem2  26481  chtub  26512  fsumvma  26513  fsumvma2  26514  chpchtsum  26519  dchrelbas2  26537  bposlem7  26590  lgsneg  26621  lgsne0  26635  lgsprme0  26639  lgsqrlem2  26647  lgsquadlem1  26680  lgsquadlem2  26681  2lgs  26707  2lgsoddprm  26716  2sqreultb  26759  istrkg3ld  27232  tgcgr4  27302  iscgra1  27581  isleag  27618  iseqlg  27638  axcontlem7  27748  elntg2  27763  edg0iedg0  27835  ausgrusgrb  27945  usgr1v0edg  28034  nb3grprlem2  28158  uvtx01vtx  28174  cplgr3v  28212  vtxd0nedgb  28265  vtxdusgr0edgnelALT  28273  1egrvtxdg0  28288  upgr2wlk  28445  wlkp1lem8  28457  wwlksnextbi  28668  s3wwlks2on  28730  elwwlks2  28740  elwspths2spth  28741  rusgrnumwwlkl1  28742  clwwlkwwlksb  28827  0pth  28898  upgriseupth  28980  eupth2lem2  28992  eupth2lem3lem4  29004  eupth2lem3lem6  29006  nfrgr2v  29045  frgr3v  29048  fusgr2wsp2nb  29107  fusgreg2wsp  29109  extwwlkfab  29125  numclwwlk2lem1  29149  frgrreggt1  29166  imsmetlem  29461  ipz  29490  bnsscmcl  29639  minvecolem4  29651  hvsubcan  29845  hoeq2  30602  leoptri  30907  atcv0eq  31150  elimifd  31294  ressupprn  31432  gtiso  31441  2ndpreima  31448  fpwrelmapffslem  31475  xnn01gt  31501  fzsplit3  31523  isomnd  31735  ogrpinvlt  31757  islinds5  31982  grplsmid  32011  smatrcl  32189  rhmpreimacnlem  32277  pstmfval  32289  lmlim  32340  dya2ub  32682  eulerpartlemr  32786  isrrvv  32855  ballotlemsima  32927  signsvfn  33006  subfacp1lem3  33588  subfacp1lem5  33590  erdszelem1  33597  erdsze  33608  erdsze2lem2  33610  satf0op  33783  fmlafvel  33791  isfmlasuc  33794  naddasslem1  34248  naddasslem2  34249  lrrecval2  34255  filnetlem4  34791  bj-issetwt  35279  bj-sbceqgALT  35307  bj-raldifsn  35509  bj-idreseq  35571  bj-elid6  35579  bj-imdirval3  35593  bj-imdirco  35599  poimirlem24  36040  itg2addnclem2  36068  ftc1anclem1  36089  areacirclem1  36104  areacirclem5  36108  metf1o  36152  isass  36243  rngosn3  36321  brxrn  36774  lsatcv0eq  37447  cmtbr2N  37653  atlatmstc  37719  1cvrco  37873  cdleme3  38638  cdleme7  38650  cdlemg10c  39040  dvhopellsm  39518  dibord  39560  dib1dim2  39569  diblsmopel  39572  dihopelvalcpre  39649  dih1dimatlem  39730  hdmap14lem13  40281  hdmapoc  40332  elrfirn  40927  jm2.19lem2  41223  pwfi2f1o  41332  proot1ex  41437  isoeq145d  41602  sqrtcval  41824  brfvidRP  41871  uneqsn  42208  ntrclsfveq  42245  ntrclskb  42252  ntrclsk3  42253  ntrneiel2  42269  k0004lem3  42332  bcc0  42531  pwpwuni  43176  disjinfi  43317  rnmptbd2  43382  rnmptbd  43389  infxrbnd2  43508  ltmulneg  43532  ltdiv23neg  43534  rexabsle  43559  uzub  43571  supxrleubrnmptf  43591  supminfxr  43604  limsupre2lem  43866  limsupre2mpt  43872  limsupre3mpt  43876  limsupreuz  43879  limsuplt2  43895  liminflimsupclim  43949  xlimpnfxnegmnf  43956  liminfpnfuz  43958  xlimclim  43966  xlimbr  43969  xlimclim2lem  43981  xlimmnfmpt  43985  xlimpnfmpt  43986  fourierdlem113  44361  isvonmbl  44780  reuf1odnf  45240  addsubeq0  45429  ltnltne  45432  iccpartgtl  45519  iccpartleu  45521  iccpartgel  45522  reuprpr  45616  fmtnoprmfac1  45658  fmtnoprmfac2  45660  quad1  45713  requad1  45715  requad2  45716  bits0ALTV  45772  bgoldbtbndlem1  45898  0nodd  46005  2nodd  46007  rngcinv  46180  rngcinvALTV  46192  ringcinv  46231  ringcinvALTV  46255  islindeps  46435  snlindsntor  46453  blen1b  46575  nn0sumshdiglem1  46608  0aryfvalel  46621  rrx2plordisom  46710  ehl2eudis0lt  46713  eenglngeehlnmlem2  46725  rrx2linest  46729  line2  46739  line2x  46741  line2y  46742  itschlc0xyqsol1  46753  itsclquadeu  46764  map0cor  46822  joindm2  46902  meetdm2  46904