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:  sbceqalOLD  3852  2reu4lem  4522  elimhyp3v  4593  elimhyp4v  4594  keephyp3v  4599  ralsng  4675  opeqsng  5508  snopeqop  5511  frsn  5773  f1eq123d  6840  foeq123d  6841  f1oeq123d  6842  fnmptfvd  7061  fnotovb  7483  ofrfvalg  7705  eloprabi  8088  fnmpoovd  8112  suppsnop  8203  smoeq  8390  naddasslem1  8732  naddasslem2  8733  mapsnend  9076  infglbb  9531  wemapwe  9737  fseqenlem1  10064  dfac12lem2  10185  fin23lem22  10367  pwfseqlem5  10703  pwfseq  10704  enqbreq2  10960  lterpq  11010  ltdiv23  12159  lediv23  12160  negfi  12217  halfpos  12496  addltmul  12502  div4p1lem1div2  12521  supminf  12977  supxrbnd1  13363  supxrbnd2  13364  iccf1o  13536  fzshftral  13655  fzoshftral  13823  2tnp1ge0ge0  13869  dfceil2  13879  modirr  13983  hashen1  14409  seqcoll  14503  hash2prb  14511  hashle2prv  14517  hash3tpb  14534  s111  14653  swrdspsleq  14703  pfxnd0  14726  pfxeq  14734  wrd2ind  14761  2swrd2eqwrdeq  14992  eqwrds3  15000  limsupgle  15513  tanaddlem  16202  dvdssub  16341  addmodlteqALT  16362  dvdsmod  16366  oddp1even  16381  nn0o1gt2  16418  nn0oddm1d2  16422  bitscmp  16475  saddisjlem  16501  smueqlem  16527  ncoprmgcdne1b  16687  cncongr1  16704  cncongr2  16705  prmreclem5  16958  4sqlem11  16993  4sqlem17  16999  vdwmc2  17017  ismre  17633  acsfn  17702  dfiso2  17816  brcic  17842  isssc  17864  setcinv  18135  cat1  18142  intopsn  18667  sgrp1  18742  sgrppropd  18744  sgrp2nmndlem4  18941  nmzsubg  19183  eqg0subg  19214  conjnmzb  19271  gsmsymgreqlem2  19449  symgfixels  19452  f1omvdconj  19464  oddvdsnn0  19562  oddvds  19565  odcong  19567  odf1  19580  dpjeq  20079  pgpfac1lem2  20095  ring1  20307  rngcinv  20637  ringcinv  20671  lsmspsn  21083  lbsacsbs  21158  rngqiprngimf1lem  21304  lpigen  21345  prmirredlem  21483  znf1o  21570  znleval  21573  znunit  21582  islinds2  21833  islindf4  21858  psdmul  22170  scmatf1  22537  isclo  23095  maxlp  23155  1stccn  23471  xkoinjcn  23695  elmptrab  23835  fbunfip  23877  elfm  23955  fmid  23968  flfnei  23999  isflf  24001  isfcls  24017  fclsopn  24022  isfcf  24042  cnextfun  24072  eltsms  24141  prdsxmetlem  24378  elmopn  24452  metss  24521  comet  24526  elbl4  24576  metuel2  24578  nrmmetd  24587  metdsge  24871  tcphcph  25271  fmcfil  25306  cmscsscms  25407  rrxmet  25442  minveclem4  25466  shft2rab  25543  sca2rab  25547  volsup2  25640  mbfsup  25699  i1fmullem  25729  mbfi1fseqlem4  25753  xrge0f  25766  itg2monolem1  25785  ellimc2  25912  cnlimc  25923  mdegleb  26103  r1pid2  26201  facth1  26206  ulm2  26428  sineq0  26566  coseq1  26567  efeq1  26570  sinord  26576  root1eq1  26798  angrtmuld  26851  affineequiv3  26868  quad2  26882  dcubic  26889  cubic2  26891  dquartlem1  26894  dquart  26896  quart  26904  rlimcnp  27008  lgamucov  27081  mumullem2  27223  chtub  27256  fsumvma  27257  fsumvma2  27258  chpchtsum  27263  dchrelbas2  27281  bposlem7  27334  lgsneg  27365  lgsne0  27379  lgsprme0  27383  lgsqrlem2  27391  lgsquadlem1  27424  lgsquadlem2  27425  2lgs  27451  2lgsoddprm  27460  2sqreultb  27503  lrrecval2  27973  istrkg3ld  28469  tgcgr4  28539  iscgra1  28818  isleag  28855  iseqlg  28875  axcontlem7  28985  elntg2  29000  edg0iedg0  29072  ausgrusgrb  29182  usgr1v0edg  29274  nb3grprlem2  29398  uvtx01vtx  29414  cplgr3v  29452  vtxd0nedgb  29506  vtxdusgr0edgnelALT  29514  1egrvtxdg0  29529  upgr2wlk  29686  wlkp1lem8  29698  dfpth2  29749  wwlksnextbi  29914  s3wwlks2on  29976  elwwlks2  29986  elwspths2spth  29987  rusgrnumwwlkl1  29988  clwwlkwwlksb  30073  0pth  30144  upgriseupth  30226  eupth2lem2  30238  eupth2lem3lem4  30250  eupth2lem3lem6  30252  nfrgr2v  30291  frgr3v  30294  fusgr2wsp2nb  30353  fusgreg2wsp  30355  extwwlkfab  30371  numclwwlk2lem1  30395  frgrreggt1  30412  imsmetlem  30709  ipz  30738  bnsscmcl  30887  minvecolem4  30899  hvsubcan  31093  hoeq2  31850  leoptri  32155  atcv0eq  32398  elimifd  32556  fdifsupp  32694  ressupprn  32699  gtiso  32710  2ndpreima  32717  fpwrelmapffslem  32743  quad3d  32754  xnn01gt  32774  fzsplit3  32795  fzo0opth  32807  isomnd  33078  ogrpinvlt  33100  islinds5  33395  grplsmid  33432  r1pid2OLD  33629  fldextrspunlsp  33724  constrsuc  33779  smatrcl  33795  rhmpreimacnlem  33883  pstmfval  33895  lmlim  33946  dya2ub  34272  eulerpartlemr  34376  isrrvv  34445  ballotlemsima  34518  signsvfn  34597  subfacp1lem3  35187  subfacp1lem5  35189  erdszelem1  35196  erdsze  35207  erdsze2lem2  35209  satf0op  35382  fmlafvel  35390  isfmlasuc  35393  filnetlem4  36382  bj-issetwt  36876  bj-sbceqgALT  36903  bj-raldifsn  37101  bj-idreseq  37163  bj-elid6  37171  bj-imdirval3  37185  bj-imdirco  37191  poimirlem24  37651  itg2addnclem2  37679  ftc1anclem1  37700  areacirclem1  37715  areacirclem5  37719  metf1o  37762  isass  37853  rngosn3  37931  brxrn  38375  lsatcv0eq  39048  cmtbr2N  39254  atlatmstc  39320  1cvrco  39474  cdleme3  40239  cdleme7  40251  cdlemg10c  40641  dvhopellsm  41119  dibord  41161  dib1dim2  41170  diblsmopel  41173  dihopelvalcpre  41250  dih1dimatlem  41331  hdmap14lem13  41882  hdmapoc  41933  cxp112d  42377  cxp111d  42378  elrfirn  42706  jm2.19lem2  43002  pwfi2f1o  43108  proot1ex  43208  isoeq145d  43432  sqrtcval  43654  brfvidRP  43701  uneqsn  44038  ntrclsfveq  44075  ntrclskb  44082  ntrclsk3  44083  ntrneiel2  44099  k0004lem3  44162  bcc0  44359  pwpwuni  45062  disjinfi  45197  rnmptbd2  45256  rnmptbd  45263  infxrbnd2  45380  ltmulneg  45403  ltdiv23neg  45405  rexabsle  45430  uzub  45442  supxrleubrnmptf  45462  supminfxr  45475  limsupre2lem  45739  limsupre2mpt  45745  limsupre3mpt  45749  limsupreuz  45752  limsuplt2  45768  liminflimsupclim  45822  xlimpnfxnegmnf  45829  liminfpnfuz  45831  xlimclim  45839  xlimbr  45842  xlimclim2lem  45854  xlimmnfmpt  45858  xlimpnfmpt  45859  fourierdlem113  46234  isvonmbl  46653  reuf1odnf  47119  addsubeq0  47308  ltnltne  47311  iccpartgtl  47413  iccpartleu  47415  iccpartgel  47416  reuprpr  47510  fmtnoprmfac1  47552  fmtnoprmfac2  47554  quad1  47607  requad1  47609  requad2  47610  bits0ALTV  47666  bgoldbtbndlem1  47792  clnbgrel  47815  clnbupgrel  47821  dfsclnbgr6  47844  isubgredg  47852  opgpgvtx  48010  gpg3kgrtriexlem5  48043  0nodd  48086  2nodd  48088  rngcinvALTV  48192  ringcinvALTV  48226  islindeps  48370  snlindsntor  48388  blen1b  48509  nn0sumshdiglem1  48542  0aryfvalel  48555  rrx2plordisom  48644  ehl2eudis0lt  48647  eenglngeehlnmlem2  48659  rrx2linest  48663  line2  48673  line2x  48675  line2y  48676  itschlc0xyqsol1  48687  itsclquadeu  48698  map0cor  48764  joindm2  48865  meetdm2  48867