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  4467  elimhyp3v  4538  elimhyp4v  4539  keephyp3v  4544  ralsng  4623  opeqsng  5438  snopeqop  5441  frsn  5699  f1eq123d  6750  foeq123d  6751  f1oeq123d  6752  fnmptfvd  6969  fnotovb  7393  ofrfvalg  7613  eloprabi  7990  fnmpoovd  8012  suppsnop  8103  smoeq  8265  naddasslem1  8604  naddasslem2  8605  mapsnend  8953  infglbb  9371  wemapwe  9582  fseqenlem1  9910  dfac12lem2  10031  fin23lem22  10213  pwfseqlem5  10549  pwfseq  10550  enqbreq2  10806  lterpq  10856  ltdiv23  12008  lediv23  12009  negfi  12066  halfpos  12346  addltmul  12352  div4p1lem1div2  12371  supminf  12828  supxrbnd1  13215  supxrbnd2  13216  iccf1o  13391  fzshftral  13510  fzoshftral  13682  2tnp1ge0ge0  13728  dfceil2  13738  modirr  13844  hashen1  14272  seqcoll  14366  hash2prb  14374  hashle2prv  14380  hash3tpb  14397  s111  14518  swrdspsleq  14568  pfxnd0  14591  pfxeq  14598  wrd2ind  14625  2swrd2eqwrdeq  14855  eqwrds3  14863  limsupgle  15379  tanaddlem  16070  difmod0  16193  dvdssub  16210  addmodlteqALT  16231  dvdsmod  16235  oddp1even  16250  nn0o1gt2  16287  nn0oddm1d2  16291  bitscmp  16344  saddisjlem  16370  smueqlem  16396  ncoprmgcdne1b  16556  cncongr1  16573  cncongr2  16574  prmreclem5  16827  4sqlem11  16862  4sqlem17  16868  vdwmc2  16886  ismre  17487  acsfn  17560  dfiso2  17674  brcic  17700  isssc  17722  setcinv  17992  cat1  17999  intopsn  18557  sgrp1  18632  sgrppropd  18634  sgrp2nmndlem4  18831  nmzsubg  19072  eqg0subg  19103  conjnmzb  19160  gsmsymgreqlem2  19338  symgfixels  19341  f1omvdconj  19353  oddvdsnn0  19451  oddvds  19454  odcong  19456  odf1  19469  dpjeq  19968  pgpfac1lem2  19984  isomnd  20030  ogrpinvlt  20051  ring1  20223  rngcinv  20547  ringcinv  20581  lsmspsn  21013  lbsacsbs  21088  rngqiprngimf1lem  21226  lpigen  21267  prmirredlem  21404  znf1o  21483  znleval  21486  znunit  21495  islinds2  21745  islindf4  21770  psdmul  22076  scmatf1  22441  isclo  22997  maxlp  23057  1stccn  23373  xkoinjcn  23597  elmptrab  23737  fbunfip  23779  elfm  23857  fmid  23870  flfnei  23901  isflf  23903  isfcls  23919  fclsopn  23924  isfcf  23944  cnextfun  23974  eltsms  24043  prdsxmetlem  24278  elmopn  24352  metss  24418  comet  24423  elbl4  24473  metuel2  24475  nrmmetd  24484  metdsge  24760  tcphcph  25159  fmcfil  25194  cmscsscms  25295  rrxmet  25330  minveclem4  25354  shft2rab  25431  sca2rab  25435  volsup2  25528  mbfsup  25587  i1fmullem  25617  mbfi1fseqlem4  25641  xrge0f  25654  itg2monolem1  25673  ellimc2  25800  cnlimc  25811  mdegleb  25991  r1pid2  26089  facth1  26094  ulm2  26316  sineq0  26455  coseq1  26456  efeq1  26459  sinord  26465  root1eq1  26687  angrtmuld  26740  affineequiv3  26757  quad2  26771  dcubic  26778  cubic2  26780  dquartlem1  26783  dquart  26785  quart  26793  rlimcnp  26897  lgamucov  26970  mumullem2  27112  chtub  27145  fsumvma  27146  fsumvma2  27147  chpchtsum  27152  dchrelbas2  27170  bposlem7  27223  lgsneg  27254  lgsne0  27268  lgsprme0  27272  lgsqrlem2  27280  lgsquadlem1  27313  lgsquadlem2  27314  2lgs  27340  2lgsoddprm  27349  2sqreultb  27392  lrrecval2  27878  subscan1d  28037  n0slem1lt  28288  istrkg3ld  28434  tgcgr4  28504  iscgra1  28783  isleag  28820  iseqlg  28840  axcontlem7  28943  elntg2  28958  edg0iedg0  29028  ausgrusgrb  29138  usgr1v0edg  29230  nb3grprlem2  29354  uvtx01vtx  29370  cplgr3v  29408  vtxd0nedgb  29462  vtxdusgr0edgnelALT  29470  1egrvtxdg0  29485  upgr2wlk  29640  wlkp1lem8  29652  dfpth2  29702  wwlksnextbi  29867  s3wwlks2on  29929  elwwlks2  29939  elwspths2spth  29940  rusgrnumwwlkl1  29941  clwwlkwwlksb  30026  0pth  30097  upgriseupth  30179  eupth2lem2  30191  eupth2lem3lem4  30203  eupth2lem3lem6  30205  nfrgr2v  30244  frgr3v  30247  fusgr2wsp2nb  30306  fusgreg2wsp  30308  extwwlkfab  30324  numclwwlk2lem1  30348  frgrreggt1  30365  imsmetlem  30662  ipz  30691  bnsscmcl  30840  minvecolem4  30852  hvsubcan  31046  hoeq2  31803  leoptri  32108  atcv0eq  32351  elimifd  32515  fdifsupp  32658  ressupprn  32663  gtiso  32674  2ndpreima  32681  fpwrelmapffslem  32707  quad3d  32725  xnn01gt  32745  fzsplit3  32768  fzo0opth  32777  islinds5  33324  grplsmid  33361  r1pid2OLD  33561  fldextrspunlsp  33679  constrsuc  33743  smatrcl  33801  rhmpreimacnlem  33889  pstmfval  33901  lmlim  33952  dya2ub  34275  eulerpartlemr  34379  isrrvv  34448  ballotlemsima  34521  signsvfn  34587  subfacp1lem3  35218  subfacp1lem5  35220  erdszelem1  35227  erdsze  35238  erdsze2lem2  35240  satf0op  35413  fmlafvel  35421  isfmlasuc  35424  filnetlem4  36415  bj-issetwt  36909  bj-sbceqgALT  36936  bj-raldifsn  37134  bj-idreseq  37196  bj-elid6  37204  bj-imdirval3  37218  bj-imdirco  37224  poimirlem24  37684  itg2addnclem2  37712  ftc1anclem1  37733  areacirclem1  37748  areacirclem5  37752  metf1o  37795  isass  37886  rngosn3  37964  brxrn  38402  lsatcv0eq  39086  cmtbr2N  39292  atlatmstc  39358  1cvrco  39511  cdleme3  40276  cdleme7  40288  cdlemg10c  40678  dvhopellsm  41156  dibord  41198  dib1dim2  41207  diblsmopel  41210  dihopelvalcpre  41287  dih1dimatlem  41368  hdmap14lem13  41919  hdmapoc  41970  cxp112d  42374  cxp111d  42375  elrfirn  42728  jm2.19lem2  43023  pwfi2f1o  43129  proot1ex  43229  isoeq145d  43452  sqrtcval  43674  brfvidRP  43721  uneqsn  44058  ntrclsfveq  44095  ntrclskb  44102  ntrclsk3  44103  ntrneiel2  44119  k0004lem3  44182  bcc0  44373  pwpwuni  45094  disjinfi  45229  rnmptbd2  45286  rnmptbd  45293  infxrbnd2  45407  ltmulneg  45430  ltdiv23neg  45432  rexabsle  45457  uzub  45469  supxrleubrnmptf  45489  supminfxr  45502  limsupre2lem  45762  limsupre2mpt  45768  limsupre3mpt  45772  limsupreuz  45775  limsuplt2  45791  liminflimsupclim  45845  xlimpnfxnegmnf  45852  liminfpnfuz  45854  xlimclim  45862  xlimbr  45865  xlimclim2lem  45877  xlimmnfmpt  45881  xlimpnfmpt  45882  fourierdlem113  46257  isvonmbl  46676  reuf1odnf  47138  addsubeq0  47327  ltnltne  47330  ceilbi  47364  iccpartgtl  47457  iccpartleu  47459  iccpartgel  47460  reuprpr  47554  fmtnoprmfac1  47596  fmtnoprmfac2  47598  quad1  47651  requad1  47653  requad2  47654  bits0ALTV  47710  bgoldbtbndlem1  47836  clnbgrel  47859  clnbupgrel  47865  dfsclnbgr6  47889  isubgredg  47897  gpgiedgdmel  48080  opgpgvtx  48086  gpg3kgrtriexlem5  48118  0nodd  48201  2nodd  48203  rngcinvALTV  48307  ringcinvALTV  48341  islindeps  48485  snlindsntor  48503  blen1b  48620  nn0sumshdiglem1  48653  0aryfvalel  48666  rrx2plordisom  48755  ehl2eudis0lt  48758  eenglngeehlnmlem2  48770  rrx2linest  48774  line2  48784  line2x  48786  line2y  48787  itschlc0xyqsol1  48798  itsclquadeu  48809  map0cor  48886  joindm2  48999  meetdm2  49001  islmd  49697  iscmd  49698