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  4784  inimasn  6176  isof1oidb  7344  oacan  8586  ecdmn0  8794  wemapwe  9737  ttrclselem2  9766  r1pw  9885  adderpqlem  10994  mulerpqlem  10995  lterpq  11010  ltanq  11011  genpass  11049  readdcan  11435  lemuldiv  12148  msq11  12169  avglt2  12505  qbtwnre  13241  iooshf  13466  clim2c  15541  lo1o1  15568  climabs0  15621  reef11  16155  absefib  16234  efieq1re  16235  nndivides  16300  oddnn02np1  16385  oddge22np1  16386  evennn02n  16387  evennn2n  16388  halfleoddlt  16399  pc2dvds  16917  pcmpt  16930  subsubc  17898  ghmqusker  19305  odmulgid  19572  gexdvds  19602  submcmn2  19857  obslbs  21750  cnntr  23283  cndis  23299  cnindis  23300  cnpdis  23301  lmres  23308  cmpfi  23416  ist0-4  23737  txhmeo  23811  tsmssubm  24151  blin  24431  cncfmet  24935  icopnfcnv  24973  lmmbrf  25296  iscauf  25314  causs  25332  mbfposr  25687  itg2gt0  25795  limcflf  25916  limcres  25921  lhop1  26053  dvdsr1p  26203  fsumvma2  27258  vmasum  27260  chpchtsum  27263  bposlem1  27328  addscan2  28026  slesubaddd  28123  mulscan2dlem  28204  iscgrgd  28521  tgcgr4  28539  lnrot1  28631  eqeelen  28919  nbusgreledg  29370  nb3grprlem2  29398  wspthsnwspthsnon  29936  rusgrnumwwlks  29994  clwwlkwwlksb  30073  clwwlknwwlksnb  30074  dmdmd  32319  nfpconfp  32642  funcnvmpt  32677  1stpreimas  32715  xrdifh  32782  swrdrn3  32940  lsmsnorb  33419  fldextrspunlsp  33724  rhmpreimacnlem  33883  ismntop  34027  eulerpartlemgh  34380  signslema  34577  fmlafvel  35390  topdifinfindis  37347  leceifl  37616  lindsadd  37620  lindsenlbs  37622  iblabsnclem  37690  ftc1anclem6  37705  areacirclem5  37719  areacirc  37720  brcoss3  38434  lsatfixedN  39010  cdlemg10c  40641  diaglbN  41057  dih1  41288  dihglbcpreN  41302  mapdcv  41662  dvdsexpnn0  42369  ef11d  42375  ellz1  42778  islssfg  43082  proot1ex  43208  tfsconcat00  43360  eliooshift  45519  clim2cf  45665  dfatdmfcoafv2  47266  sfprmdvdsmersenne  47590  odd2np1ALTV  47661  vopnbgrelself  47841  rrx2plordisom  48644  i0oii  48817  io1ii  48818