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  6120  funcnvmpt  6949  isof1oidb  7279  oacan  8483  ecdmn0  8696  wemapwe  9618  ttrclselem2  9647  r1pw  9769  adderpqlem  10877  mulerpqlem  10878  lterpq  10893  ltanq  10894  genpass  10932  readdcan  11320  lemuldiv  12036  msq11  12057  avglt2  12416  qbtwnre  13151  iooshf  13379  clim2c  15467  lo1o1  15494  climabs0  15547  reef11  16086  absefib  16165  efieq1re  16166  nndivides  16231  oddnn02np1  16317  oddge22np1  16318  evennn02n  16319  evennn2n  16320  halfleoddlt  16331  pc2dvds  16850  pcmpt  16863  subsubc  17820  ghmqusker  19262  odmulgid  19529  gexdvds  19559  submcmn2  19814  obslbs  21710  cnntr  23240  cndis  23256  cnindis  23257  cnpdis  23258  lmres  23265  cmpfi  23373  ist0-4  23694  txhmeo  23768  tsmssubm  24108  blin  24386  cncfmet  24876  icopnfcnv  24909  lmmbrf  25229  iscauf  25247  causs  25265  mbfposr  25619  itg2gt0  25727  limcflf  25848  limcres  25853  lhop1  25981  dvdsr1p  26129  fsumvma2  27177  vmasum  27179  chpchtsum  27182  bposlem1  27247  addscan2  27985  lesubaddsd  28085  mulscan2dlem  28170  bdayfinbndlem1  28459  iscgrgd  28581  tgcgr4  28599  lnrot1  28691  eqeelen  28973  nbusgreledg  29422  nb3grprlem2  29450  wspthsnwspthsnon  29984  rusgrnumwwlks  30045  clwwlkwwlksb  30124  clwwlknwwlksnb  30125  dmdmd  32371  nfpconfp  32705  1stpreimas  32779  xrdifh  32853  swrdrn3  33015  lsmsnorb  33451  esplyfval1  33717  fldextrspunlsp  33818  rhmpreimacnlem  34028  ismntop  34170  eulerpartlemgh  34522  signslema  34706  fmlafvel  35567  topdifinfindis  37662  leceifl  37930  lindsadd  37934  lindsenlbs  37936  iblabsnclem  38004  ftc1anclem6  38019  areacirclem5  38033  areacirc  38034  brcoss3  38844  lsatfixedN  39455  cdlemg10c  41085  diaglbN  41501  dih1  41732  dihglbcpreN  41746  mapdcv  42106  dvdsexpnn0  42766  ef11d  42771  ellz1  43199  islssfg  43498  proot1ex  43624  tfsconcat00  43775  eliooshift  45936  clim2cf  46078  dfatdmfcoafv2  47702  sfprmdvdsmersenne  48066  odd2np1ALTV  48150  vopnbgrelself  48331  rrx2plordisom  49199  i0oii  49395  io1ii  49396  oppccic  49519  uptrlem3  49687  uptr2  49696