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:  2reu4lem  4485  elimhyp3v  4556  elimhyp4v  4557  keephyp3v  4562  ralsng  4639  opeqsng  5463  snopeqop  5466  frsn  5726  f1eq123d  6792  foeq123d  6793  f1oeq123d  6794  fnmptfvd  7013  fnotovb  7439  ofrfvalg  7661  eloprabi  8042  fnmpoovd  8066  suppsnop  8157  smoeq  8319  naddasslem1  8658  naddasslem2  8659  mapsnend  9007  infglbb  9443  wemapwe  9650  fseqenlem1  9977  dfac12lem2  10098  fin23lem22  10280  pwfseqlem5  10616  pwfseq  10617  enqbreq2  10873  lterpq  10923  ltdiv23  12074  lediv23  12075  negfi  12132  halfpos  12412  addltmul  12418  div4p1lem1div2  12437  supminf  12894  supxrbnd1  13281  supxrbnd2  13282  iccf1o  13457  fzshftral  13576  fzoshftral  13745  2tnp1ge0ge0  13791  dfceil2  13801  modirr  13907  hashen1  14335  seqcoll  14429  hash2prb  14437  hashle2prv  14443  hash3tpb  14460  s111  14580  swrdspsleq  14630  pfxnd0  14653  pfxeq  14661  wrd2ind  14688  2swrd2eqwrdeq  14919  eqwrds3  14927  limsupgle  15443  tanaddlem  16134  difmod0  16257  dvdssub  16274  addmodlteqALT  16295  dvdsmod  16299  oddp1even  16314  nn0o1gt2  16351  nn0oddm1d2  16355  bitscmp  16408  saddisjlem  16434  smueqlem  16460  ncoprmgcdne1b  16620  cncongr1  16637  cncongr2  16638  prmreclem5  16891  4sqlem11  16926  4sqlem17  16932  vdwmc2  16950  ismre  17551  acsfn  17620  dfiso2  17734  brcic  17760  isssc  17782  setcinv  18052  cat1  18059  intopsn  18581  sgrp1  18656  sgrppropd  18658  sgrp2nmndlem4  18855  nmzsubg  19097  eqg0subg  19128  conjnmzb  19185  gsmsymgreqlem2  19361  symgfixels  19364  f1omvdconj  19376  oddvdsnn0  19474  oddvds  19477  odcong  19479  odf1  19492  dpjeq  19991  pgpfac1lem2  20007  ring1  20219  rngcinv  20546  ringcinv  20580  lsmspsn  20991  lbsacsbs  21066  rngqiprngimf1lem  21204  lpigen  21245  prmirredlem  21382  znf1o  21461  znleval  21464  znunit  21473  islinds2  21722  islindf4  21747  psdmul  22053  scmatf1  22418  isclo  22974  maxlp  23034  1stccn  23350  xkoinjcn  23574  elmptrab  23714  fbunfip  23756  elfm  23834  fmid  23847  flfnei  23878  isflf  23880  isfcls  23896  fclsopn  23901  isfcf  23921  cnextfun  23951  eltsms  24020  prdsxmetlem  24256  elmopn  24330  metss  24396  comet  24401  elbl4  24451  metuel2  24453  nrmmetd  24462  metdsge  24738  tcphcph  25137  fmcfil  25172  cmscsscms  25273  rrxmet  25308  minveclem4  25332  shft2rab  25409  sca2rab  25413  volsup2  25506  mbfsup  25565  i1fmullem  25595  mbfi1fseqlem4  25619  xrge0f  25632  itg2monolem1  25651  ellimc2  25778  cnlimc  25789  mdegleb  25969  r1pid2  26067  facth1  26072  ulm2  26294  sineq0  26433  coseq1  26434  efeq1  26437  sinord  26443  root1eq1  26665  angrtmuld  26718  affineequiv3  26735  quad2  26749  dcubic  26756  cubic2  26758  dquartlem1  26761  dquart  26763  quart  26771  rlimcnp  26875  lgamucov  26948  mumullem2  27090  chtub  27123  fsumvma  27124  fsumvma2  27125  chpchtsum  27130  dchrelbas2  27148  bposlem7  27201  lgsneg  27232  lgsne0  27246  lgsprme0  27250  lgsqrlem2  27258  lgsquadlem1  27291  lgsquadlem2  27292  2lgs  27318  2lgsoddprm  27327  2sqreultb  27370  lrrecval2  27847  subscan1d  28006  n0slem1lt  28257  istrkg3ld  28388  tgcgr4  28458  iscgra1  28737  isleag  28774  iseqlg  28794  axcontlem7  28897  elntg2  28912  edg0iedg0  28982  ausgrusgrb  29092  usgr1v0edg  29184  nb3grprlem2  29308  uvtx01vtx  29324  cplgr3v  29362  vtxd0nedgb  29416  vtxdusgr0edgnelALT  29424  1egrvtxdg0  29439  upgr2wlk  29596  wlkp1lem8  29608  dfpth2  29659  wwlksnextbi  29824  s3wwlks2on  29886  elwwlks2  29896  elwspths2spth  29897  rusgrnumwwlkl1  29898  clwwlkwwlksb  29983  0pth  30054  upgriseupth  30136  eupth2lem2  30148  eupth2lem3lem4  30160  eupth2lem3lem6  30162  nfrgr2v  30201  frgr3v  30204  fusgr2wsp2nb  30263  fusgreg2wsp  30265  extwwlkfab  30281  numclwwlk2lem1  30305  frgrreggt1  30322  imsmetlem  30619  ipz  30648  bnsscmcl  30797  minvecolem4  30809  hvsubcan  31003  hoeq2  31760  leoptri  32065  atcv0eq  32308  elimifd  32472  fdifsupp  32608  ressupprn  32613  gtiso  32624  2ndpreima  32631  fpwrelmapffslem  32655  quad3d  32673  xnn01gt  32693  fzsplit3  32716  fzo0opth  32728  isomnd  33015  ogrpinvlt  33037  islinds5  33338  grplsmid  33375  r1pid2OLD  33574  fldextrspunlsp  33669  constrsuc  33728  smatrcl  33786  rhmpreimacnlem  33874  pstmfval  33886  lmlim  33937  dya2ub  34261  eulerpartlemr  34365  isrrvv  34434  ballotlemsima  34507  signsvfn  34573  subfacp1lem3  35169  subfacp1lem5  35171  erdszelem1  35178  erdsze  35189  erdsze2lem2  35191  satf0op  35364  fmlafvel  35372  isfmlasuc  35375  filnetlem4  36369  bj-issetwt  36863  bj-sbceqgALT  36890  bj-raldifsn  37088  bj-idreseq  37150  bj-elid6  37158  bj-imdirval3  37172  bj-imdirco  37178  poimirlem24  37638  itg2addnclem2  37666  ftc1anclem1  37687  areacirclem1  37702  areacirclem5  37706  metf1o  37749  isass  37840  rngosn3  37918  brxrn  38356  lsatcv0eq  39040  cmtbr2N  39246  atlatmstc  39312  1cvrco  39466  cdleme3  40231  cdleme7  40243  cdlemg10c  40633  dvhopellsm  41111  dibord  41153  dib1dim2  41162  diblsmopel  41165  dihopelvalcpre  41242  dih1dimatlem  41323  hdmap14lem13  41874  hdmapoc  41925  cxp112d  42329  cxp111d  42330  elrfirn  42683  jm2.19lem2  42979  pwfi2f1o  43085  proot1ex  43185  isoeq145d  43408  sqrtcval  43630  brfvidRP  43677  uneqsn  44014  ntrclsfveq  44051  ntrclskb  44058  ntrclsk3  44059  ntrneiel2  44075  k0004lem3  44138  bcc0  44329  pwpwuni  45051  disjinfi  45186  rnmptbd2  45243  rnmptbd  45250  infxrbnd2  45365  ltmulneg  45388  ltdiv23neg  45390  rexabsle  45415  uzub  45427  supxrleubrnmptf  45447  supminfxr  45460  limsupre2lem  45722  limsupre2mpt  45728  limsupre3mpt  45732  limsupreuz  45735  limsuplt2  45751  liminflimsupclim  45805  xlimpnfxnegmnf  45812  liminfpnfuz  45814  xlimclim  45822  xlimbr  45825  xlimclim2lem  45837  xlimmnfmpt  45841  xlimpnfmpt  45842  fourierdlem113  46217  isvonmbl  46636  reuf1odnf  47108  addsubeq0  47297  ltnltne  47300  ceilbi  47334  iccpartgtl  47427  iccpartleu  47429  iccpartgel  47430  reuprpr  47524  fmtnoprmfac1  47566  fmtnoprmfac2  47568  quad1  47621  requad1  47623  requad2  47624  bits0ALTV  47680  bgoldbtbndlem1  47806  clnbgrel  47829  clnbupgrel  47835  dfsclnbgr6  47858  isubgredg  47866  gpgiedgdmel  48040  opgpgvtx  48046  gpg3kgrtriexlem5  48078  0nodd  48158  2nodd  48160  rngcinvALTV  48264  ringcinvALTV  48298  islindeps  48442  snlindsntor  48460  blen1b  48577  nn0sumshdiglem1  48610  0aryfvalel  48623  rrx2plordisom  48712  ehl2eudis0lt  48715  eenglngeehlnmlem2  48727  rrx2linest  48731  line2  48741  line2x  48743  line2y  48744  itschlc0xyqsol1  48755  itsclquadeu  48766  map0cor  48843  joindm2  48956  meetdm2  48958  islmd  49654  iscmd  49655