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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  inimasn  6098  isof1oidb  7253  oacan  8458  ecdmn0  8669  wemapwe  9582  ttrclselem2  9611  r1pw  9733  adderpqlem  10840  mulerpqlem  10841  lterpq  10856  ltanq  10857  genpass  10895  readdcan  11282  lemuldiv  11997  msq11  12018  avglt2  12355  qbtwnre  13093  iooshf  13321  clim2c  15407  lo1o1  15434  climabs0  15487  reef11  16023  absefib  16102  efieq1re  16103  nndivides  16168  oddnn02np1  16254  oddge22np1  16255  evennn02n  16256  evennn2n  16257  halfleoddlt  16268  pc2dvds  16786  pcmpt  16799  subsubc  17755  ghmqusker  19194  odmulgid  19461  gexdvds  19491  submcmn2  19746  obslbs  21662  cnntr  23185  cndis  23201  cnindis  23202  cnpdis  23203  lmres  23210  cmpfi  23318  ist0-4  23639  txhmeo  23713  tsmssubm  24053  blin  24331  cncfmet  24824  icopnfcnv  24862  lmmbrf  25184  iscauf  25202  causs  25220  mbfposr  25575  itg2gt0  25683  limcflf  25804  limcres  25809  lhop1  25941  dvdsr1p  26091  fsumvma2  27147  vmasum  27149  chpchtsum  27152  bposlem1  27217  addscan2  27931  slesubaddd  28028  mulscan2dlem  28112  iscgrgd  28486  tgcgr4  28504  lnrot1  28596  eqeelen  28877  nbusgreledg  29326  nb3grprlem2  29354  wspthsnwspthsnon  29889  rusgrnumwwlks  29947  clwwlkwwlksb  30026  clwwlknwwlksnb  30027  dmdmd  32272  nfpconfp  32606  funcnvmpt  32641  1stpreimas  32679  xrdifh  32755  swrdrn3  32928  lsmsnorb  33348  fldextrspunlsp  33679  rhmpreimacnlem  33889  ismntop  34031  eulerpartlemgh  34383  signslema  34567  fmlafvel  35421  topdifinfindis  37380  leceifl  37649  lindsadd  37653  lindsenlbs  37655  iblabsnclem  37723  ftc1anclem6  37738  areacirclem5  37752  areacirc  37753  brcoss3  38470  lsatfixedN  39048  cdlemg10c  40678  diaglbN  41094  dih1  41325  dihglbcpreN  41339  mapdcv  41699  dvdsexpnn0  42367  ef11d  42372  ellz1  42800  islssfg  43103  proot1ex  43229  tfsconcat00  43380  eliooshift  45546  clim2cf  45688  dfatdmfcoafv2  47285  sfprmdvdsmersenne  47634  odd2np1ALTV  47705  vopnbgrelself  47886  rrx2plordisom  48755  i0oii  48951  io1ii  48952  oppccic  49076  uptrlem3  49244  uptr2  49253