Theorem 3bitr4rd 313

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  inimasn  6114  funcnvmpt  6944  isof1oidb  7275  oacan  8480  ecdmn0  8693  wemapwe  9616  ttrclselem2  9645  r1pw  9767  adderpqlem  10875  mulerpqlem  10876  lterpq  10891  ltanq  10892  genpass  10930  readdcan  11318  lemuldiv  12034  msq11  12055  avglt2  12414  qbtwnre  13149  iooshf  13377  clim2c  15465  lo1o1  15492  climabs0  15545  reef11  16084  absefib  16163  efieq1re  16164  nndivides  16229  oddnn02np1  16315  oddge22np1  16316  evennn02n  16317  evennn2n  16318  halfleoddlt  16329  pc2dvds  16848  pcmpt  16861  subsubc  17818  ghmqusker  19260  odmulgid  19527  gexdvds  19557  submcmn2  19812  obslbs  21712  cnntr  23265  cndis  23281  cnindis  23282  cnpdis  23283  lmres  23290  cmpfi  23398  ist0-4  23719  txhmeo  23793  tsmssubm  24133  blin  24411  cncfmet  24901  icopnfcnv  24934  lmmbrf  25254  iscauf  25272  causs  25290  mbfposr  25644  itg2gt0  25752  limcflf  25873  limcres  25878  lhop1  26006  dvdsr1p  26154  fsumvma2  27202  vmasum  27204  chpchtsum  27207  bposlem1  27272  addscan2  28010  lesubaddsd  28110  mulscan2dlem  28195  bdayfinbndlem1  28484  iscgrgd  28606  tgcgr4  28624  lnrot1  28716  eqeelen  28998  nbusgreledg  29447  nb3grprlem2  29475  wspthsnwspthsnon  30009  rusgrnumwwlks  30070  clwwlkwwlksb  30149  clwwlknwwlksnb  30150  dmdmd  32396  nfpconfp  32731  1stpreimas  32805  xrdifh  32879  swrdrn3  33041  lsmsnorb  33481  esplyfval1  33764  fldextrspunlsp  33865  rhmpreimacnlem  34075  ismntop  34217  eulerpartlemgh  34569  signslema  34753  fmlafvel  35620  topdifinfindis  37715  leceifl  37983  lindsadd  37987  lindsenlbs  37989  iblabsnclem  38057  ftc1anclem6  38072  areacirclem5  38086  areacirc  38087  brcoss3  38897  lsatfixedN  39508  cdlemg10c  41138  diaglbN  41554  dih1  41785  dihglbcpreN  41799  mapdcv  42159  dvdsexpnn0  42818  ef11d  42823  ellz1  43223  islssfg  43522  proot1ex  43648  tfsconcat00  43799  eliooshift  45958  clim2cf  46100  dfatdmfcoafv2  47724  sfprmdvdsmersenne  48088  odd2np1ALTV  48172  vopnbgrelself  48353  rrx2plordisom  49221  i0oii  49417  io1ii  49418  oppccic  49541  uptrlem3  49709  uptr2  49718