Theorem 3bitr4rd 312

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr4d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3bitr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3bitr4rd	⊢ (𝜑 → (𝜏 ↔ 𝜃))

Proof of Theorem 3bitr4rd

Step	Hyp	Ref	Expression
1		3bitr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
2		3bitr4d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitr4d 281	. 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓))
4		3bitr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	3, 4	bitr4d 281	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:  snssg  4719  inimasn  6064  isof1oidb  7204  oacan  8388  ecdmn0  8554  wemapwe  9464  ttrclselem2  9493  r1pw  9612  adderpqlem  10719  mulerpqlem  10720  lterpq  10735  ltanq  10736  genpass  10774  readdcan  11158  lemuldiv  11864  msq11  11885  avglt2  12221  qbtwnre  12942  iooshf  13167  clim2c  15223  lo1o1  15250  climabs0  15303  reef11  15837  absefib  15916  efieq1re  15917  nndivides  15982  oddnn02np1  16066  oddge22np1  16067  evennn02n  16068  evennn2n  16069  halfleoddlt  16080  pc2dvds  16589  pcmpt  16602  subsubc  17577  odmulgid  19170  gexdvds  19198  submcmn2  19449  obslbs  20946  cnntr  22435  cndis  22451  cnindis  22452  cnpdis  22453  lmres  22460  cmpfi  22568  ist0-4  22889  txhmeo  22963  tsmssubm  23303  blin  23583  cncfmet  24081  icopnfcnv  24114  lmmbrf  24435  iscauf  24453  causs  24471  mbfposr  24825  itg2gt0  24934  limcflf  25054  limcres  25059  lhop1  25187  dvdsr1p  25335  fsumvma2  26371  vmasum  26373  chpchtsum  26376  bposlem1  26441  iscgrgd  26883  tgcgr4  26901  lnrot1  26993  eqeelen  27281  nbusgreledg  27729  nb3grprlem2  27757  wspthsnwspthsnon  28290  rusgrnumwwlks  28348  clwwlkwwlksb  28427  clwwlknwwlksnb  28428  dmdmd  30671  nfpconfp  30976  funcnvmpt  31013  1stpreimas  31047  xrdifh  31110  swrdrn3  31236  lsmsnorb  31588  rhmpreimacnlem  31843  ismntop  31985  eulerpartlemgh  32354  signslema  32550  fmlafvel  33356  topdifinfindis  35526  leceifl  35775  lindsadd  35779  lindsenlbs  35781  iblabsnclem  35849  ftc1anclem6  35864  areacirclem5  35878  areacirc  35879  brcoss3  36563  lsatfixedN  37030  cdlemg10c  38660  diaglbN  39076  dih1  39307  dihglbcpreN  39321  mapdcv  39681  dvdsexpnn0  40348  ellz1  40596  islssfg  40902  proot1ex  41033  eliooshift  43051  clim2cf  43198  dfatdmfcoafv2  44757  sfprmdvdsmersenne  45066  odd2np1ALTV  45137  rrx2plordisom  46080  i0oii  46224  io1ii  46225