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  6100  isof1oidb  7253  oacan  8458  ecdmn0  8669  wemapwe  9582  ttrclselem2  9611  r1pw  9730  adderpqlem  10837  mulerpqlem  10838  lterpq  10853  ltanq  10854  genpass  10892  readdcan  11279  lemuldiv  11994  msq11  12015  avglt2  12352  qbtwnre  13090  iooshf  13318  clim2c  15404  lo1o1  15431  climabs0  15484  reef11  16020  absefib  16099  efieq1re  16100  nndivides  16165  oddnn02np1  16251  oddge22np1  16252  evennn02n  16253  evennn2n  16254  halfleoddlt  16265  pc2dvds  16783  pcmpt  16796  subsubc  17752  ghmqusker  19192  odmulgid  19459  gexdvds  19489  submcmn2  19744  obslbs  21660  cnntr  23183  cndis  23199  cnindis  23200  cnpdis  23201  lmres  23208  cmpfi  23316  ist0-4  23637  txhmeo  23711  tsmssubm  24051  blin  24329  cncfmet  24822  icopnfcnv  24860  lmmbrf  25182  iscauf  25200  causs  25218  mbfposr  25573  itg2gt0  25681  limcflf  25802  limcres  25807  lhop1  25939  dvdsr1p  26089  fsumvma2  27145  vmasum  27147  chpchtsum  27150  bposlem1  27215  addscan2  27929  slesubaddd  28026  mulscan2dlem  28110  iscgrgd  28484  tgcgr4  28502  lnrot1  28594  eqeelen  28875  nbusgreledg  29324  nb3grprlem2  29352  wspthsnwspthsnon  29887  rusgrnumwwlks  29945  clwwlkwwlksb  30024  clwwlknwwlksnb  30025  dmdmd  32270  nfpconfp  32604  funcnvmpt  32639  1stpreimas  32677  xrdifh  32753  swrdrn3  32926  lsmsnorb  33346  fldextrspunlsp  33677  rhmpreimacnlem  33887  ismntop  34029  eulerpartlemgh  34381  signslema  34565  fmlafvel  35397  topdifinfindis  37359  leceifl  37628  lindsadd  37632  lindsenlbs  37634  iblabsnclem  37702  ftc1anclem6  37717  areacirclem5  37731  areacirc  37732  brcoss3  38449  lsatfixedN  39027  cdlemg10c  40657  diaglbN  41073  dih1  41304  dihglbcpreN  41318  mapdcv  41678  dvdsexpnn0  42346  ef11d  42351  ellz1  42779  islssfg  43082  proot1ex  43208  tfsconcat00  43359  eliooshift  45525  clim2cf  45667  dfatdmfcoafv2  47264  sfprmdvdsmersenne  47613  odd2np1ALTV  47684  vopnbgrelself  47865  rrx2plordisom  48734  i0oii  48930  io1ii  48931  oppccic  49055  uptrlem3  49223  uptr2  49232