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  4479  elimhyp3v  4550  elimhyp4v  4551  keephyp3v  4556  ralsng  4636  opeqsng  5480  snopeqop  5483  frsn  5743  f1eq123d  6809  foeq123d  6810  f1oeq123d  6811  fnmptfvd  7033  fnotovb  7465  ofrfvalg  7686  eloprabi  8060  fnmpoovd  8084  suppsnop  8176  smoeq  8339  naddasslem1  8683  naddasslem2  8684  mapsnend  9043  infglbb  9462  wemapwe  9676  fseqenlem1  10027  dfac12lem2  10147  fin23lem22  10329  pwfseqlem5  10672  pwfseq  10673  enqbreq2  10929  lterpq  10979  ltdiv23  12130  lediv23  12131  negfi  12188  halfpos  12498  addltmul  12504  div4p1lem1div2  12523  supminf  12984  supxrbnd1  13373  supxrbnd2  13374  iccf1o  13549  fzshftral  13670  fzoshftral  13843  2tnp1ge0ge0  13890  dfceil2  13900  modirr  14006  hashen1  14434  seqcoll  14529  hash2prb  14537  hashle2prv  14543  hash3tpb  14560  s111  14683  swrdspsleq  14735  pfxnd0  14758  pfxeq  14765  wrd2ind  14792  2swrd2eqwrdeq  15026  eqwrds3  15034  limsupgle  15564  tanaddlem  16254  difmod0  16377  dvdssub  16394  addmodlteqALT  16415  dvdsmod  16419  oddp1even  16434  nn0o1gt2  16471  nn0oddm1d2  16475  bitscmp  16528  saddisjlem  16554  smueqlem  16580  ncoprmgcdne1b  16740  cncongr1  16757  cncongr2  16758  prmreclem5  17012  4sqlem11  17047  4sqlem17  17053  vdwmc2  17071  ismre  17674  acsfn  17747  dfiso2  17861  brcic  17887  isssc  17909  setcinv  18179  cat1  18186  intopsn  18746  sgrp1  18831  sgrppropd  18833  sgrp2nmndlem4  19040  nmzsubg  19288  eqg0subg  19324  conjnmzb  19380  gsmsymgreqlem2  19558  symgfixels  19561  f1omvdconj  19573  oddvdsnn0  19671  oddvds  19674  odcong  19676  odf1  19689  dpjeq  20188  pgpfac1lem2  20204  isomnd  20250  ogrpinvlt  20271  ring1  20452  rngcinv  20799  ringcinv  20833  lsmspsn  21268  lbsacsbs  21343  rngqiprngimf1lem  21497  lpigen  21566  prmirredlem  21685  znf1o  21764  znleval  21767  znunit  21776  islinds2  22026  islindf4  22051  psdmul  22394  scmatf1  22753  isclo  23312  maxlp  23372  1stccn  23689  xkoinjcn  23913  elmptrab  24053  fbunfip  24095  elfm  24173  fmid  24186  flfnei  24217  isflf  24219  isfcls  24235  fclsopn  24240  isfcf  24260  cnextfun  24290  eltsms  24359  prdsxmetlem  24594  elmopn  24668  metss  24734  comet  24739  elbl4  24789  metuel2  24791  nrmmetd  24800  metdsge  25076  tcphcph  25465  fmcfil  25500  cmscsscms  25601  rrxmet  25636  minveclem4  25660  shft2rab  25736  sca2rab  25740  volsup2  25833  mbfsup  25892  i1fmullem  25922  mbfi1fseqlem4  25946  xrge0f  25959  itg2monolem1  25978  ellimc2  26104  cnlimc  26115  mdegleb  26289  r1pid2  26387  facth1  26392  rnplynfin  26539  ulm2  26621  sineq0  26761  coseq1  26762  efeq1  26765  sinord  26771  root1eq1  26992  angrtmuld  27045  affineequiv3  27062  quad2  27076  dcubic  27083  cubic2  27085  dquartlem1  27088  dquart  27090  quart  27098  rlimcnp  27202  lgamucov  27274  mumullem2  27416  chtub  27448  fsumvma  27449  fsumvma2  27450  chpchtsum  27455  dchrelbas2  27473  bposlem7  27526  lgsneg  27557  lgsne0  27571  lgsprme0  27575  lgsqrlem2  27583  lgsquadlem1  27616  lgsquadlem2  27617  2lgs  27643  2lgsoddprm  27652  2sqreultb  27695  lrrecval2  28205  subscan1d  28368  n0lesm1lt  28632  bdaypw2bnd  28730  elreno2  28760  istrkg3ld  28802  tgcgr4  28873  iscgra1  29196  isleag  29245  iseqlg  29291  axcontlem7  29427  elntg2  29442  edg0iedg0  29512  ausgrusgrb  29625  usgr1v0edg  29717  nb3grprlem2  29841  uvtx01vtx  29857  cplgr3v  29895  vtxd0nedgb  29948  vtxdusgr0edgnelALT  29956  1egrvtxdg0  29971  upgr2wlk  30126  wlkp1lem8  30138  dfpth2  30193  wwlksnextbi  30362  s3wwlks2on  30424  sps3wwlks2on  30425  elwwlks2  30437  elwspths2spth  30438  rusgrnumwwlkl1  30439  clwwlkwwlksb  30524  0pth  30595  upgriseupth  30687  eupth2lem2  30699  eupth2lem3lem4  30711  eupth2lem3lem6  30713  nfrgr2v  30752  frgr3v  30755  fusgr2wsp2nb  30814  fusgreg2wsp  30816  extwwlkfab  30832  numclwwlk2lem1  30856  frgrreggt1  30873  imsmetlem  31171  ipz  31200  bnsscmcl  31349  minvecolem4  31361  hvsubcan  31555  hoeq2  32312  leoptri  32617  atcv0eq  32860  elimifd  33018  fdifsupp  33157  ressupprn  33162  gtiso  33173  2ndpreima  33180  fpwrelmapffslem  33203  quad3d  33220  xnn01gt  33241  fzsplit3  33264  fzo0opth  33274  rlocisunit  33716  islinds5  33802  grplsmid  33833  selvply1rhmlem2  34031  fldextrspunlsp  34184  constrsuc  34248  smatrcl  34306  rhmpreimacnlem  34394  pstmfval  34406  lmlim  34457  dya2ub  34781  eulerpartlemr  34885  isrrvv  34954  ballotlemsima  35027  signsvfn  35090  subfacp1lem3  35761  subfacp1lem5  35763  erdszelem1  35770  erdsze  35781  erdsze2lem2  35783  satf0op  35956  fmlafvel  35964  isfmlasuc  35967  filnetlem4  37000  bj-issetwt  37618  bj-sbceqgALT  37645  bj-raldifsn  37850  bj-idreseq  37914  bj-elid6  37922  bj-imdirval3  37936  bj-imdirco  37942  poimirlem24  38393  itg2addnclem2  38421  ftc1anclem1  38442  areacirclem1  38457  areacirclem5  38461  metf1o  38505  isass  38596  rngosn3  38674  brxrn  39131  lsatcv0eq  39920  cmtbr2N  40126  atlatmstc  40192  1cvrco  40345  cdleme3  41110  cdleme7  41122  cdlemg10c  41512  dvhopellsm  41990  dibord  42032  dib1dim2  42041  diblsmopel  42044  dihopelvalcpre  42121  dih1dimatlem  42202  hdmap14lem13  42753  hdmapoc  42804  quadfac  43071  cxp112d  43216  cxp111d  43217  elrfirn  43540  jm2.19lem2  43831  pwfi2f1o  43937  proot1ex  44037  isoeq145d  44259  sqrtcval  44481  brfvidRP  44528  uneqsn  44865  ntrclsfveq  44902  ntrclskb  44909  ntrclsk3  44910  ntrneiel2  44926  k0004lem3  44989  bcc0  45164  pwpwuni  45891  disjinfi  46024  rnmptbd2  46078  rnmptbd  46085  infxrbnd2  46198  ltmulneg  46221  ltdiv23neg  46223  rexabsle  46247  uzub  46259  supxrleubrnmptf  46279  supminfxr  46292  limsupre2lem  46552  limsupre2mpt  46558  limsupre3mpt  46562  limsupreuz  46565  limsuplt2  46581  liminflimsupclim  46635  xlimpnfxnegmnf  46642  liminfpnfuz  46644  xlimclim  46652  xlimbr  46655  xlimclim2lem  46667  xlimmnfmpt  46671  xlimpnfmpt  46672  fourierdlem113  47047  isvonmbl  47466  chnsubseqwl  47707  reuf1odnf  47995  addsubeq0  48184  ltnltne  48187  ceilbi  48225  iccpartgtl  48326  iccpartleu  48328  iccpartgel  48329  reuprpr  48423  fmtnoprmfac1  48468  fmtnoprmfac2  48470  quad1  48536  requad1  48538  requad2  48539  bits0ALTV  48595  bgoldbtbndlem1  48721  clnbgrel  48744  clnbupgrel  48750  dfsclnbgr6  48774  isubgredg  48782  gpgiedgdmel  48965  opgpgvtx  48971  gpg3kgrtriexlem5  49003  0nodd  49085  2nodd  49087  rngcinvALTV  49191  ringcinvALTV  49225  crngprmringidom  49256  islindeps  49383  snlindsntor  49401  blen1b  49518  nn0sumshdiglem1  49551  0aryfvalel  49564  rrx2plordisom  49653  ehl2eudis0lt  49656  eenglngeehlnmlem2  49668  rrx2linest  49672  line2  49682  line2x  49684  line2y  49685  itschlc0xyqsol1  49696  itsclquadeu  49707  map0cor  49783  joindm2  49894  meetdm2  49896  islmd  50591  iscmd  50592