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  6155  funcnvmpt  6993  isof1oidb  7324  oacan  8534  ecdmn0  8748  wemapwe  9667  ttrclselem2  9696  r1pw  9818  adderpqlem  10940  mulerpqlem  10941  lterpq  10956  ltanq  10957  genpass  10995  readdcan  11385  lemuldiv  12096  msq11  12117  avglt2  12484  qbtwnre  13226  iooshf  13454  clim2c  15558  lo1o1  15585  climabs0  15638  reef11  16176  absefib  16255  efieq1re  16256  nndivides  16321  oddnn02np1  16407  oddge22np1  16408  evennn02n  16409  evennn2n  16410  halfleoddlt  16421  pc2dvds  16940  pcmpt  16953  subsubc  17911  ghmqusker  19358  odmulgid  19625  gexdvds  19655  submcmn2  19910  obslbs  21861  cnntr  23413  cndis  23429  cnindis  23430  cnpdis  23431  lmres  23438  cmpfi  23546  ist0-4  23867  txhmeo  23941  tsmssubm  24281  blin  24559  cncfmet  25049  icopnfcnv  25082  lmmbrf  25402  iscauf  25420  causs  25438  mbfposr  25792  itg2gt0  25900  limcflf  26021  limcres  26026  lhop1  26154  dvdsr1p  26302  fsumvma2  27359  vmasum  27361  chpchtsum  27364  bposlem1  27429  addscan2  28167  lesubaddsd  28267  mulscan2dlem  28352  bdayfinbndlem1  28641  iscgrgd  28763  tgcgr4  28781  lnrot1  28877  dfprlng2  29178  eqeelen  29235  nbusgreledg  29684  nb3grprlem2  29712  wspthsnwspthsnon  30246  rusgrnumwwlks  30307  clwwlkwwlksb  30386  clwwlknwwlksnb  30387  dmdmd  32633  nfpconfp  32958  1stpreimas  33032  xrdifh  33106  swrdrn3  33256  lsmsnorb  33685  esplyfval1  33944  fldextrspunlsp  34045  rhmpreimacnlem  34255  ismntop  34397  eulerpartlemgh  34749  signslema  34930  fmlafvel  35858  topdifinfindis  37973  leceifl  38241  lindsadd  38245  lindsenlbs  38247  iblabsnclem  38315  ftc1anclem6  38330  areacirclem5  38344  areacirc  38345  brcoss3  39153  lsatfixedN  39764  cdlemg10c  41394  diaglbN  41810  dih1  42041  dihglbcpreN  42055  mapdcv  42415  dvdsexpnn0  43076  ef11d  43081  ellz1  43481  islssfg  43780  proot1ex  43906  tfsconcat00  44057  eliooshift  46205  clim2cf  46347  dfatdmfcoafv2  47974  sfprmdvdsmersenne  48338  odd2np1ALTV  48422  vopnbgrelself  48603  rrx2plordisom  49486  i0oii  49681  io1ii  49682  oppccic  49805  uptrlem3  49973  uptr2  49982