Theorem 3bitr4rd 315

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  inimasn  6152  funcnvmpt  6989  isof1oidb  7320  oacan  8529  ecdmn0  8743  wemapwe  9662  ttrclselem2  9691  r1pw  9813  adderpqlem  10935  mulerpqlem  10936  lterpq  10951  ltanq  10952  genpass  10990  readdcan  11380  lemuldiv  12091  msq11  12112  avglt2  12479  qbtwnre  13221  iooshf  13449  clim2c  15552  lo1o1  15579  climabs0  15632  reef11  16171  absefib  16250  efieq1re  16251  nndivides  16316  oddnn02np1  16402  oddge22np1  16403  evennn02n  16404  evennn2n  16405  halfleoddlt  16416  pc2dvds  16935  pcmpt  16948  subsubc  17906  ghmqusker  19353  odmulgid  19620  gexdvds  19650  submcmn2  19905  obslbs  21845  cnntr  23397  cndis  23413  cnindis  23414  cnpdis  23415  lmres  23422  cmpfi  23530  ist0-4  23851  txhmeo  23925  tsmssubm  24265  blin  24543  cncfmet  25033  icopnfcnv  25066  lmmbrf  25386  iscauf  25404  causs  25422  mbfposr  25776  itg2gt0  25884  limcflf  26005  limcres  26010  lhop1  26138  dvdsr1p  26286  fsumvma2  27340  vmasum  27342  chpchtsum  27345  bposlem1  27410  addscan2  28148  lesubaddsd  28248  mulscan2dlem  28333  bdayfinbndlem1  28622  iscgrgd  28744  tgcgr4  28762  lnrot1  28854  eqeelen  29191  nbusgreledg  29640  nb3grprlem2  29668  wspthsnwspthsnon  30202  rusgrnumwwlks  30263  clwwlkwwlksb  30342  clwwlknwwlksnb  30343  dmdmd  32589  nfpconfp  32914  1stpreimas  32988  xrdifh  33062  swrdrn3  33212  lsmsnorb  33644  esplyfval1  33904  fldextrspunlsp  34005  rhmpreimacnlem  34215  ismntop  34357  eulerpartlemgh  34709  signslema  34890  fmlafvel  35772  topdifinfindis  37875  leceifl  38143  lindsadd  38147  lindsenlbs  38149  iblabsnclem  38217  ftc1anclem6  38232  areacirclem5  38246  areacirc  38247  brcoss3  39057  lsatfixedN  39668  cdlemg10c  41298  diaglbN  41714  dih1  41945  dihglbcpreN  41959  mapdcv  42319  dvdsexpnn0  42978  ef11d  42983  ellz1  43383  islssfg  43682  proot1ex  43808  tfsconcat00  43959  eliooshift  46107  clim2cf  46249  dfatdmfcoafv2  47873  sfprmdvdsmersenne  48237  odd2np1ALTV  48321  vopnbgrelself  48502  rrx2plordisom  49381  i0oii  49576  io1ii  49577  oppccic  49700  uptrlem3  49868  uptr2  49877