Theorem 3bitrd 296

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 270	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 270	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  sbceqal  3685  elimhyp3v  4344  elimhyp4v  4345  keephyp3v  4350  opeqsng  5156  snopeqop  5160  frsn  5391  opelresg  5603  elpredg  5907  f1eq123d  6347  foeq123d  6348  f1oeq123d  6349  fnmptfvd  6542  fnotovb  6923  ofrfval  7135  eloprabi  7465  fnmpt2ovd  7485  fnmpt2ovdOLD  7486  suppsnop  7543  smoeq  7683  mapsnend  8271  infglbb  8636  wemapwe  8841  fseqenlem1  9130  dfac12lem2  9251  fin23lem22  9434  pwfseqlem5  9770  pwfseq  9771  enqbreq2  10027  lterpq  10077  ltdiv23  11199  lediv23  11200  negfi  11256  halfpos  11529  addltmul  11535  div4p1lem1div2  11554  supminf  11994  supxrbnd1  12369  supxrbnd2  12370  iccf1o  12539  fzshftral  12651  fzoshftral  12809  2tnp1ge0ge0  12854  dfceil2  12864  modirr  12965  hashen1  13378  seqcoll  13465  hash2prb  13471  hashle2prv  13477  ccat0  13573  s111  13610  swrdeq  13668  wrd2ind  13701  2swrd2eqwrdeq  13921  eqwrds3  13929  limsupgle  14431  tanaddlem  15116  dvdssub  15249  addmodlteqALT  15270  dvdsmod  15273  oddp1even  15288  nn0o1gt2  15317  nn0oddm1d2  15321  bitscmp  15379  saddisjlem  15405  smueqlem  15431  ncoprmgcdne1b  15582  cncongr1  15599  cncongr2  15600  prmreclem5  15841  4sqlem11  15876  4sqlem17  15882  vdwmc2  15900  ismre  16455  acsfn  16524  dfiso2  16636  brcic  16662  isssc  16684  setcinv  16944  intopsn  17458  sgrp1  17498  sgrp2nmndlem4  17620  nmzsubg  17837  conjnmzb  17897  gsmsymgreqlem2  18052  symgfixels  18055  f1omvdconj  18067  oddvdsnn0  18164  oddvds  18167  odcong  18169  odf1  18180  dpjeq  18660  pgpfac1lem2  18676  ring1  18804  lsmspsn  19291  lbsacsbs  19365  lpigen  19465  prmirredlem  20049  znf1o  20107  znleval  20110  znunit  20119  islinds2  20362  islindf4  20387  scmatf1  20548  isclo  21105  maxlp  21165  1stccn  21480  xkoinjcn  21704  elmptrab  21844  fbunfip  21886  elfm  21964  fmid  21977  flfnei  22008  isflf  22010  isfcls  22026  fclsopn  22031  isfcf  22051  cnextfun  22081  eltsms  22149  prdsxmetlem  22386  elmopn  22460  metss  22526  comet  22531  elbl4  22581  metuel2  22583  nrmmetd  22592  metdsge  22865  tchcph  23248  fmcfil  23282  rrxmet  23403  minveclem4  23415  shft2rab  23489  sca2rab  23493  volsup2  23586  mbfsup  23645  i1fmullem  23675  mbfi1fseqlem4  23699  xrge0f  23712  itg2monolem1  23731  ellimc2  23855  cnlimc  23866  mdegleb  24038  facth1  24138  ulm2  24353  sineq0  24488  coseq1  24489  efeq1  24490  sinord  24495  root1eq1  24710  angrtmuld  24752  quad2  24780  dcubic  24787  cubic2  24789  dquartlem1  24792  dquart  24794  quart  24802  rlimcnp  24906  lgamucov  24978  mumullem2  25120  chtub  25151  fsumvma  25152  fsumvma2  25153  chpchtsum  25158  bposlem7  25229  lgsneg  25260  lgsne0  25274  lgsprme0  25278  lgsqrlem2  25286  lgsquadlem1  25319  lgsquadlem2  25320  2lgs  25346  2lgsoddprm  25355  istrkg3ld  25574  tgcgr4  25640  iscgra1  25916  isleag  25947  iseqlg  25961  axcontlem7  26064  edg0iedg0  26163  edg0iedg0OLD  26164  ausgrusgrb  26275  usgr1v0edg  26365  nb3grprlem2  26499  uvtx01vtx  26518  uvtxa01vtx0OLD  26520  cplgr3v  26559  vtxd0nedgb  26612  vtxdusgr0edgnelALT  26620  1egrvtxdg0  26635  wlkeq  26757  upgr2wlk  26792  wlkp1lem8  26805  wwlksnextbi  27031  wspthsnwspthsnonOLD  27056  s3wwlks2on  27097  elwwlks2  27108  elwspths2spth  27109  rusgrnumwwlkl1  27110  0pth  27298  upgriseupth  27380  eupth2lem2  27392  eupth2lem3lem4  27404  eupth2lem3lem6  27406  nfrgr2v  27447  frgr3v  27450  fusgr2wsp2nb  27509  fusgreg2wsp  27511  extwwlkfab  27531  numclwwlk2lem1  27556  numclwwlk2lem1OLD  27563  frgrreggt1  27581  imsmetlem  27873  ipz  27902  bnsscmcl  28052  minvecolem4  28064  hvsubcan  28259  hoeq2  29018  leoptri  29323  atcv0eq  29566  elimifd  29687  gtiso  29805  2ndpreima  29812  fpwrelmapffslem  29834  fzsplit3  29880  isomnd  30026  ogrpinvlt  30049  smatrcl  30187  pstmfval  30264  lmlim  30318  dya2ub  30657  eulerpartlemr  30761  isrrvv  30830  ballotlemsima  30902  signsvfn  30984  subfacp1lem3  31487  subfacp1lem5  31489  erdszelem1  31496  erdsze  31507  erdsze2lem2  31509  filnetlem4  32697  bj-issetwt  33167  bj-sbceqgALT  33205  bj-raldifsn  33365  csbwrecsg  33490  poimirlem24  33746  itg2addnclem2  33774  ftc1anclem1  33797  areacirclem1  33812  areacirclem5  33816  metf1o  33862  isass  33956  rngosn3  34034  brxrn  34449  lsatcv0eq  34827  cmtbr2N  35033  atlatmstc  35099  1cvrco  35252  cdleme3  36018  cdleme7  36030  cdlemg10c  36420  dvhopellsm  36898  dibord  36940  dib1dim2  36949  diblsmopel  36952  dihopelvalcpre  37029  dih1dimatlem  37110  hdmap14lem13  37661  hdmapoc  37712  elrfirn  37760  jm2.19lem2  38058  pwfi2f1o  38167  proot1ex  38280  brfvidRP  38480  uneqsn  38821  ntrclsfveq  38860  ntrclskb  38867  ntrclsk3  38868  ntrneiel2  38884  k0004lem3  38947  bcc0  39039  pwpwuni  39718  rnmptpr  39847  disjinfi  39869  rnmptbd2  39947  rnmptbd  39954  infxrbnd2  40065  ltmulneg  40094  ltdiv23neg  40096  rexabsle  40125  uzub  40137  supxrleubrnmptf  40159  supminfxr  40173  limsupre2lem  40436  limsupre2mpt  40442  limsupre3mpt  40446  limsupreuz  40449  limsuplt2  40465  liminflimsupclim  40519  xlimclim  40530  xlimbr  40533  xlimclim2lem  40545  xlimmnfmpt  40549  xlimpnfmpt  40550  fourierdlem113  40915  isvonmbl  41334  2reu4a  41701  ltnltne  41889  iccpartgtl  41937  iccpartleu  41939  iccpartgel  41940  pfxeq  41979  fmtnoprmfac1  42052  fmtnoprmfac2  42054  bits0ALTV  42165  bgoldbtbndlem1  42268  0nodd  42378  2nodd  42380  rngcinv  42549  rngcinvALTV  42561  ringcinv  42600  ringcinvALTV  42624  islindeps  42810  snlindsntor  42828  blen1b  42950  nn0sumshdiglem1  42983