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  3843  2reu4lem  4530  elimhyp3v  4600  elimhyp4v  4601  keephyp3v  4606  ralsng  4682  opeqsng  5509  snopeqop  5512  frsn  5769  f1eq123d  6835  foeq123d  6836  f1oeq123d  6837  fnmptfvd  7054  fnotovb  7475  ofrfvalg  7698  eloprabi  8077  fnmpoovd  8101  suppsnop  8192  smoeq  8380  naddasslem1  8724  naddasslem2  8725  mapsnend  9072  infglbb  9534  wemapwe  9740  fseqenlem1  10067  dfac12lem2  10187  fin23lem22  10370  pwfseqlem5  10706  pwfseq  10707  enqbreq2  10963  lterpq  11013  ltdiv23  12157  lediv23  12158  negfi  12215  halfpos  12494  addltmul  12500  div4p1lem1div2  12519  supminf  12971  supxrbnd1  13354  supxrbnd2  13355  iccf1o  13527  fzshftral  13643  fzoshftral  13804  2tnp1ge0ge0  13849  dfceil2  13859  modirr  13962  hashen1  14387  seqcoll  14483  hash2prb  14491  hashle2prv  14497  s111  14623  swrdspsleq  14673  pfxnd0  14696  pfxeq  14704  wrd2ind  14731  2swrd2eqwrdeq  14962  eqwrds3  14970  limsupgle  15479  tanaddlem  16168  dvdssub  16306  addmodlteqALT  16327  dvdsmod  16331  oddp1even  16346  nn0o1gt2  16383  nn0oddm1d2  16387  bitscmp  16438  saddisjlem  16464  smueqlem  16490  ncoprmgcdne1b  16651  cncongr1  16668  cncongr2  16669  prmreclem5  16922  4sqlem11  16957  4sqlem17  16963  vdwmc2  16981  ismre  17603  acsfn  17672  dfiso2  17788  brcic  17814  isssc  17836  setcinv  18112  cat1  18119  intopsn  18647  sgrp1  18722  sgrppropd  18724  sgrp2nmndlem4  18918  nmzsubg  19159  eqg0subg  19190  conjnmzb  19247  gsmsymgreqlem2  19429  symgfixels  19432  f1omvdconj  19444  oddvdsnn0  19542  oddvds  19545  odcong  19547  odf1  19560  dpjeq  20059  pgpfac1lem2  20075  ring1  20289  rngcinv  20615  ringcinv  20649  lsmspsn  21062  lbsacsbs  21137  rngqiprngimf1lem  21283  lpigen  21324  prmirredlem  21462  znf1o  21549  znleval  21552  znunit  21561  islinds2  21811  islindf4  21836  psdmul  22160  scmatf1  22524  isclo  23082  maxlp  23142  1stccn  23458  xkoinjcn  23682  elmptrab  23822  fbunfip  23864  elfm  23942  fmid  23955  flfnei  23986  isflf  23988  isfcls  24004  fclsopn  24009  isfcf  24029  cnextfun  24059  eltsms  24128  prdsxmetlem  24365  elmopn  24439  metss  24508  comet  24513  elbl4  24563  metuel2  24565  nrmmetd  24574  metdsge  24856  tcphcph  25256  fmcfil  25291  cmscsscms  25392  rrxmet  25427  minveclem4  25451  shft2rab  25528  sca2rab  25532  volsup2  25625  mbfsup  25684  i1fmullem  25714  mbfi1fseqlem4  25739  xrge0f  25752  itg2monolem1  25771  ellimc2  25897  cnlimc  25908  mdegleb  26091  r1pid2  26189  facth1  26194  ulm2  26414  sineq0  26551  coseq1  26552  efeq1  26555  sinord  26561  root1eq1  26783  angrtmuld  26836  affineequiv3  26853  quad2  26867  dcubic  26874  cubic2  26876  dquartlem1  26879  dquart  26881  quart  26889  rlimcnp  26993  lgamucov  27066  mumullem2  27208  chtub  27241  fsumvma  27242  fsumvma2  27243  chpchtsum  27248  dchrelbas2  27266  bposlem7  27319  lgsneg  27350  lgsne0  27364  lgsprme0  27368  lgsqrlem2  27376  lgsquadlem1  27409  lgsquadlem2  27410  2lgs  27436  2lgsoddprm  27445  2sqreultb  27488  lrrecval2  27954  istrkg3ld  28388  tgcgr4  28458  iscgra1  28737  isleag  28774  iseqlg  28794  axcontlem7  28904  elntg2  28919  edg0iedg0  28991  ausgrusgrb  29101  usgr1v0edg  29193  nb3grprlem2  29317  uvtx01vtx  29333  cplgr3v  29371  vtxd0nedgb  29425  vtxdusgr0edgnelALT  29433  1egrvtxdg0  29448  upgr2wlk  29605  wlkp1lem8  29617  wwlksnextbi  29828  s3wwlks2on  29890  elwwlks2  29900  elwspths2spth  29901  rusgrnumwwlkl1  29902  clwwlkwwlksb  29987  0pth  30058  upgriseupth  30140  eupth2lem2  30152  eupth2lem3lem4  30164  eupth2lem3lem6  30166  nfrgr2v  30205  frgr3v  30208  fusgr2wsp2nb  30267  fusgreg2wsp  30269  extwwlkfab  30285  numclwwlk2lem1  30309  frgrreggt1  30326  imsmetlem  30623  ipz  30652  bnsscmcl  30801  minvecolem4  30813  hvsubcan  31007  hoeq2  31764  leoptri  32069  atcv0eq  32312  elimifd  32464  ressupprn  32602  gtiso  32612  2ndpreima  32619  fpwrelmapffslem  32646  xnn01gt  32674  fzsplit3  32696  fzo0opth  32707  isomnd  32936  ogrpinvlt  32958  islinds5  33242  grplsmid  33279  r1pid2OLD  33476  constrsuc  33596  smatrcl  33611  rhmpreimacnlem  33699  pstmfval  33711  lmlim  33762  dya2ub  34104  eulerpartlemr  34208  isrrvv  34277  ballotlemsima  34349  signsvfn  34428  subfacp1lem3  35010  subfacp1lem5  35012  erdszelem1  35019  erdsze  35030  erdsze2lem2  35032  satf0op  35205  fmlafvel  35213  isfmlasuc  35216  filnetlem4  36093  bj-issetwt  36580  bj-sbceqgALT  36608  bj-raldifsn  36807  bj-idreseq  36869  bj-elid6  36877  bj-imdirval3  36891  bj-imdirco  36897  poimirlem24  37345  itg2addnclem2  37373  ftc1anclem1  37394  areacirclem1  37409  areacirclem5  37413  metf1o  37456  isass  37547  rngosn3  37625  brxrn  38072  lsatcv0eq  38745  cmtbr2N  38951  atlatmstc  39017  1cvrco  39171  cdleme3  39936  cdleme7  39948  cdlemg10c  40338  dvhopellsm  40816  dibord  40858  dib1dim2  40867  diblsmopel  40870  dihopelvalcpre  40947  dih1dimatlem  41028  hdmap14lem13  41579  hdmapoc  41630  cxp112d  42137  cxp111d  42138  elrfirn  42352  jm2.19lem2  42648  pwfi2f1o  42757  proot1ex  42861  isoeq145d  43086  sqrtcval  43308  brfvidRP  43355  uneqsn  43692  ntrclsfveq  43729  ntrclskb  43736  ntrclsk3  43737  ntrneiel2  43753  k0004lem3  43816  bcc0  44014  pwpwuni  44658  disjinfi  44799  rnmptbd2  44858  rnmptbd  44865  infxrbnd2  44984  ltmulneg  45007  ltdiv23neg  45009  rexabsle  45034  uzub  45046  supxrleubrnmptf  45066  supminfxr  45079  limsupre2lem  45345  limsupre2mpt  45351  limsupre3mpt  45355  limsupreuz  45358  limsuplt2  45374  liminflimsupclim  45428  xlimpnfxnegmnf  45435  liminfpnfuz  45437  xlimclim  45445  xlimbr  45448  xlimclim2lem  45460  xlimmnfmpt  45464  xlimpnfmpt  45465  fourierdlem113  45840  isvonmbl  46259  reuf1odnf  46720  addsubeq0  46909  ltnltne  46912  iccpartgtl  46998  iccpartleu  47000  iccpartgel  47001  reuprpr  47095  fmtnoprmfac1  47137  fmtnoprmfac2  47139  quad1  47192  requad1  47194  requad2  47195  bits0ALTV  47251  bgoldbtbndlem1  47377  clnbgrel  47399  clnbupgrel  47405  dfsclnbgr6  47425  0nodd  47547  2nodd  47549  rngcinvALTV  47653  ringcinvALTV  47687  islindeps  47836  snlindsntor  47854  blen1b  47976  nn0sumshdiglem1  48009  0aryfvalel  48022  rrx2plordisom  48111  ehl2eudis0lt  48114  eenglngeehlnmlem2  48126  rrx2linest  48130  line2  48140  line2x  48142  line2y  48143  itschlc0xyqsol1  48154  itsclquadeu  48165  map0cor  48222  joindm2  48302  meetdm2  48304