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:  snssgOLD  4809  inimasn  6187  isof1oidb  7360  oacan  8604  ecdmn0  8812  wemapwe  9766  ttrclselem2  9795  r1pw  9914  adderpqlem  11023  mulerpqlem  11024  lterpq  11039  ltanq  11040  genpass  11078  readdcan  11464  lemuldiv  12175  msq11  12196  avglt2  12532  qbtwnre  13261  iooshf  13486  clim2c  15551  lo1o1  15578  climabs0  15631  reef11  16167  absefib  16246  efieq1re  16247  nndivides  16312  oddnn02np1  16396  oddge22np1  16397  evennn02n  16398  evennn2n  16399  halfleoddlt  16410  pc2dvds  16926  pcmpt  16939  subsubc  17917  ghmqusker  19327  odmulgid  19596  gexdvds  19626  submcmn2  19881  obslbs  21773  cnntr  23304  cndis  23320  cnindis  23321  cnpdis  23322  lmres  23329  cmpfi  23437  ist0-4  23758  txhmeo  23832  tsmssubm  24172  blin  24452  cncfmet  24954  icopnfcnv  24992  lmmbrf  25315  iscauf  25333  causs  25351  mbfposr  25706  itg2gt0  25815  limcflf  25936  limcres  25941  lhop1  26073  dvdsr1p  26223  fsumvma2  27276  vmasum  27278  chpchtsum  27281  bposlem1  27346  addscan2  28044  slesubaddd  28141  mulscan2dlem  28222  iscgrgd  28539  tgcgr4  28557  lnrot1  28649  eqeelen  28937  nbusgreledg  29388  nb3grprlem2  29416  wspthsnwspthsnon  29949  rusgrnumwwlks  30007  clwwlkwwlksb  30086  clwwlknwwlksnb  30087  dmdmd  32332  nfpconfp  32651  funcnvmpt  32685  1stpreimas  32717  xrdifh  32785  swrdrn3  32922  lsmsnorb  33384  rhmpreimacnlem  33830  ismntop  33972  eulerpartlemgh  34343  signslema  34539  fmlafvel  35353  topdifinfindis  37312  leceifl  37569  lindsadd  37573  lindsenlbs  37575  iblabsnclem  37643  ftc1anclem6  37658  areacirclem5  37672  areacirc  37673  brcoss3  38389  lsatfixedN  38965  cdlemg10c  40596  diaglbN  41012  dih1  41243  dihglbcpreN  41257  mapdcv  41617  dvdsexpnn0  42321  ef11d  42327  ellz1  42723  islssfg  43027  proot1ex  43157  tfsconcat00  43309  eliooshift  45424  clim2cf  45571  dfatdmfcoafv2  47169  sfprmdvdsmersenne  47477  odd2np1ALTV  47548  vopnbgrelself  47727  rrx2plordisom  48457  i0oii  48599  io1ii  48600