Theorem 3bitr4rd 314

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  inimasn  6137  funcnvmpt  6972  isof1oidb  7303  oacan  8511  ecdmn0  8725  wemapwe  9646  ttrclselem2  9675  r1pw  9797  adderpqlem  10906  mulerpqlem  10907  lterpq  10922  ltanq  10923  genpass  10961  readdcan  11351  lemuldiv  12066  msq11  12087  avglt2  12454  qbtwnre  13196  iooshf  13424  clim2c  15523  lo1o1  15550  climabs0  15603  reef11  16142  absefib  16221  efieq1re  16222  nndivides  16287  oddnn02np1  16373  oddge22np1  16374  evennn02n  16375  evennn2n  16376  halfleoddlt  16387  pc2dvds  16906  pcmpt  16919  subsubc  17877  ghmqusker  19318  odmulgid  19585  gexdvds  19615  submcmn2  19870  obslbs  21770  cnntr  23323  cndis  23339  cnindis  23340  cnpdis  23341  lmres  23348  cmpfi  23456  ist0-4  23777  txhmeo  23851  tsmssubm  24191  blin  24469  cncfmet  24959  icopnfcnv  24992  lmmbrf  25312  iscauf  25330  causs  25348  mbfposr  25702  itg2gt0  25810  limcflf  25931  limcres  25936  lhop1  26064  dvdsr1p  26212  fsumvma2  27266  vmasum  27268  chpchtsum  27271  bposlem1  27336  addscan2  28074  lesubaddsd  28174  mulscan2dlem  28259  bdayfinbndlem1  28548  iscgrgd  28670  tgcgr4  28688  lnrot1  28780  eqeelen  29062  nbusgreledg  29511  nb3grprlem2  29539  wspthsnwspthsnon  30073  rusgrnumwwlks  30134  clwwlkwwlksb  30213  clwwlknwwlksnb  30214  dmdmd  32460  nfpconfp  32795  1stpreimas  32869  xrdifh  32943  swrdrn3  33094  lsmsnorb  33538  esplyfval1  33831  fldextrspunlsp  33932  rhmpreimacnlem  34142  ismntop  34284  eulerpartlemgh  34636  signslema  34817  fmlafvel  35696  topdifinfindis  37801  leceifl  38069  lindsadd  38073  lindsenlbs  38075  iblabsnclem  38143  ftc1anclem6  38158  areacirclem5  38172  areacirc  38173  brcoss3  38983  lsatfixedN  39594  cdlemg10c  41224  diaglbN  41640  dih1  41871  dihglbcpreN  41885  mapdcv  42245  dvdsexpnn0  42904  ef11d  42909  ellz1  43309  islssfg  43608  proot1ex  43734  tfsconcat00  43885  eliooshift  46043  clim2cf  46185  dfatdmfcoafv2  47809  sfprmdvdsmersenne  48173  odd2np1ALTV  48257  vopnbgrelself  48438  rrx2plordisom  49306  i0oii  49502  io1ii  49503  oppccic  49626  uptrlem3  49794  uptr2  49803