Theorem 3bitrd 308

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  2reu4lem  4486  elimhyp3v  4557  elimhyp4v  4558  keephyp3v  4563  ralsng  4643  opeqsng  5488  snopeqop  5491  frsn  5751  f1eq123d  6816  foeq123d  6817  f1oeq123d  6818  fnmptfvd  7040  fnotovb  7468  ofrfvalg  7688  eloprabi  8062  fnmpoovd  8084  suppsnop  8176  smoeq  8339  naddasslem1  8683  naddasslem2  8684  mapsnend  9036  infglbb  9455  wemapwe  9669  fseqenlem1  10020  dfac12lem2  10140  fin23lem22  10322  pwfseqlem5  10659  pwfseq  10660  enqbreq2  10916  lterpq  10966  ltdiv23  12117  lediv23  12118  negfi  12175  halfpos  12485  addltmul  12491  div4p1lem1div2  12510  supminf  12970  supxrbnd1  13358  supxrbnd2  13359  iccf1o  13534  fzshftral  13655  fzoshftral  13828  2tnp1ge0ge0  13875  dfceil2  13885  modirr  13991  hashen1  14419  seqcoll  14514  hash2prb  14522  hashle2prv  14528  hash3tpb  14545  s111  14668  swrdspsleq  14720  pfxnd0  14743  pfxeq  14750  wrd2ind  14777  2swrd2eqwrdeq  15009  eqwrds3  15017  limsupgle  15547  tanaddlem  16239  difmod0  16362  dvdssub  16379  addmodlteqALT  16400  dvdsmod  16404  oddp1even  16419  nn0o1gt2  16456  nn0oddm1d2  16460  bitscmp  16513  saddisjlem  16539  smueqlem  16565  ncoprmgcdne1b  16725  cncongr1  16742  cncongr2  16743  prmreclem5  16997  4sqlem11  17032  4sqlem17  17038  vdwmc2  17056  ismre  17659  acsfn  17732  dfiso2  17846  brcic  17872  isssc  17894  setcinv  18164  cat1  18171  intopsn  18729  sgrp1  18808  sgrppropd  18810  sgrp2nmndlem4  19013  nmzsubg  19254  eqg0subg  19290  conjnmzb  19346  gsmsymgreqlem2  19524  symgfixels  19527  f1omvdconj  19539  oddvdsnn0  19637  oddvds  19640  odcong  19642  odf1  19655  dpjeq  20154  pgpfac1lem2  20170  isomnd  20216  ogrpinvlt  20237  ring1  20418  rngcinv  20765  ringcinv  20799  lsmspsn  21234  lbsacsbs  21309  rngqiprngimf1lem  21463  lpigen  21532  prmirredlem  21651  znf1o  21730  znleval  21733  znunit  21742  islinds2  21992  islindf4  22017  psdmul  22358  scmatf1  22717  isclo  23273  maxlp  23333  1stccn  23649  xkoinjcn  23873  elmptrab  24013  fbunfip  24055  elfm  24133  fmid  24146  flfnei  24177  isflf  24179  isfcls  24195  fclsopn  24200  isfcf  24220  cnextfun  24250  eltsms  24319  prdsxmetlem  24554  elmopn  24628  metss  24694  comet  24699  elbl4  24749  metuel2  24751  nrmmetd  24760  metdsge  25036  tcphcph  25425  fmcfil  25460  cmscsscms  25561  rrxmet  25596  minveclem4  25620  shft2rab  25696  sca2rab  25700  volsup2  25793  mbfsup  25852  i1fmullem  25882  mbfi1fseqlem4  25906  xrge0f  25919  itg2monolem1  25938  ellimc2  26065  cnlimc  26076  mdegleb  26250  r1pid2  26348  facth1  26353  ulm2  26577  sineq0  26718  coseq1  26719  efeq1  26722  sinord  26728  root1eq1  26949  angrtmuld  27002  affineequiv3  27019  quad2  27033  dcubic  27040  cubic2  27042  dquartlem1  27045  dquart  27047  quart  27055  rlimcnp  27159  lgamucov  27231  mumullem2  27373  chtub  27405  fsumvma  27406  fsumvma2  27407  chpchtsum  27412  dchrelbas2  27430  bposlem7  27483  lgsneg  27514  lgsne0  27528  lgsprme0  27532  lgsqrlem2  27540  lgsquadlem1  27573  lgsquadlem2  27574  2lgs  27600  2lgsoddprm  27609  2sqreultb  27652  lrrecval2  28162  subscan1d  28325  n0lesm1lt  28589  bdaypw2bnd  28687  elreno2  28717  istrkg3ld  28759  tgcgr4  28829  iscgra1  29150  isleag  29193  iseqlg  29213  axcontlem7  29349  elntg2  29364  edg0iedg0  29434  ausgrusgrb  29544  usgr1v0edg  29636  nb3grprlem2  29760  uvtx01vtx  29776  cplgr3v  29814  vtxd0nedgb  29867  vtxdusgr0edgnelALT  29875  1egrvtxdg0  29890  upgr2wlk  30045  wlkp1lem8  30057  dfpth2  30107  wwlksnextbi  30272  s3wwlks2on  30334  sps3wwlks2on  30335  elwwlks2  30347  elwspths2spth  30348  rusgrnumwwlkl1  30349  clwwlkwwlksb  30434  0pth  30505  upgriseupth  30587  eupth2lem2  30599  eupth2lem3lem4  30611  eupth2lem3lem6  30613  nfrgr2v  30652  frgr3v  30655  fusgr2wsp2nb  30714  fusgreg2wsp  30716  extwwlkfab  30732  numclwwlk2lem1  30756  frgrreggt1  30773  imsmetlem  31071  ipz  31100  bnsscmcl  31249  minvecolem4  31261  hvsubcan  31455  hoeq2  32212  leoptri  32517  atcv0eq  32760  elimifd  32918  fdifsupp  33059  ressupprn  33064  gtiso  33075  2ndpreima  33082  fpwrelmapffslem  33106  quad3d  33123  xnn01gt  33144  fzsplit3  33167  fzo0opth  33177  rlocisunit  33619  islinds5  33705  grplsmid  33736  selvply1rhmlem2  33934  fldextrspunlsp  34087  constrsuc  34151  smatrcl  34209  rhmpreimacnlem  34297  pstmfval  34309  lmlim  34360  dya2ub  34684  eulerpartlemr  34788  isrrvv  34857  ballotlemsima  34930  signsvfn  34993  subfacp1lem3  35687  subfacp1lem5  35689  erdszelem1  35696  erdsze  35707  erdsze2lem2  35709  satf0op  35882  fmlafvel  35890  isfmlasuc  35893  filnetlem4  36925  bj-issetwt  37543  bj-sbceqgALT  37570  bj-raldifsn  37775  bj-idreseq  37839  bj-elid6  37847  bj-imdirval3  37861  bj-imdirco  37867  poimirlem24  38328  itg2addnclem2  38356  ftc1anclem1  38377  areacirclem1  38392  areacirclem5  38396  metf1o  38439  isass  38530  rngosn3  38608  brxrn  39065  lsatcv0eq  39854  cmtbr2N  40060  atlatmstc  40126  1cvrco  40279  cdleme3  41044  cdleme7  41056  cdlemg10c  41446  dvhopellsm  41924  dibord  41966  dib1dim2  41975  diblsmopel  41978  dihopelvalcpre  42055  dih1dimatlem  42136  hdmap14lem13  42687  hdmapoc  42738  quadfac  43005  cxp112d  43135  cxp111d  43136  elrfirn  43459  jm2.19lem2  43750  pwfi2f1o  43856  proot1ex  43956  isoeq145d  44178  sqrtcval  44400  brfvidRP  44447  uneqsn  44784  ntrclsfveq  44821  ntrclskb  44828  ntrclsk3  44829  ntrneiel2  44845  k0004lem3  44908  bcc0  45083  pwpwuni  45810  disjinfi  45943  rnmptbd2  45997  rnmptbd  46004  infxrbnd2  46117  ltmulneg  46140  ltdiv23neg  46142  rexabsle  46166  uzub  46178  supxrleubrnmptf  46198  supminfxr  46211  limsupre2lem  46471  limsupre2mpt  46477  limsupre3mpt  46481  limsupreuz  46484  limsuplt2  46500  liminflimsupclim  46554  xlimpnfxnegmnf  46561  liminfpnfuz  46563  xlimclim  46571  xlimbr  46574  xlimclim2lem  46586  xlimmnfmpt  46590  xlimpnfmpt  46591  fourierdlem113  46966  isvonmbl  47385  chnsubseqwl  47628  reuf1odnf  47877  addsubeq0  48066  ltnltne  48069  ceilbi  48107  iccpartgtl  48208  iccpartleu  48210  iccpartgel  48211  reuprpr  48305  fmtnoprmfac1  48350  fmtnoprmfac2  48352  quad1  48418  requad1  48420  requad2  48421  bits0ALTV  48477  bgoldbtbndlem1  48603  clnbgrel  48626  clnbupgrel  48632  dfsclnbgr6  48656  isubgredg  48664  gpgiedgdmel  48847  opgpgvtx  48853  gpg3kgrtriexlem5  48885  0nodd  48968  2nodd  48970  rngcinvALTV  49074  ringcinvALTV  49108  crngprmringidom  49139  islindeps  49266  snlindsntor  49284  blen1b  49401  nn0sumshdiglem1  49434  0aryfvalel  49447  rrx2plordisom  49536  ehl2eudis0lt  49539  eenglngeehlnmlem2  49551  rrx2linest  49555  line2  49565  line2x  49567  line2y  49568  itschlc0xyqsol1  49579  itsclquadeu  49590  map0cor  49666  joindm2  49779  meetdm2  49781  islmd  50476  iscmd  50477