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:  snssgOLD  4760  inimasn  6145  isof1oidb  7316  oacan  8558  ecdmn0  8766  wemapwe  9709  ttrclselem2  9738  r1pw  9857  adderpqlem  10966  mulerpqlem  10967  lterpq  10982  ltanq  10983  genpass  11021  readdcan  11407  lemuldiv  12120  msq11  12141  avglt2  12478  qbtwnre  13213  iooshf  13441  clim2c  15519  lo1o1  15546  climabs0  15599  reef11  16135  absefib  16214  efieq1re  16215  nndivides  16280  oddnn02np1  16365  oddge22np1  16366  evennn02n  16367  evennn2n  16368  halfleoddlt  16379  pc2dvds  16897  pcmpt  16910  subsubc  17864  ghmqusker  19268  odmulgid  19533  gexdvds  19563  submcmn2  19818  obslbs  21688  cnntr  23211  cndis  23227  cnindis  23228  cnpdis  23229  lmres  23236  cmpfi  23344  ist0-4  23665  txhmeo  23739  tsmssubm  24079  blin  24358  cncfmet  24851  icopnfcnv  24889  lmmbrf  25212  iscauf  25230  causs  25248  mbfposr  25603  itg2gt0  25711  limcflf  25832  limcres  25837  lhop1  25969  dvdsr1p  26119  fsumvma2  27175  vmasum  27177  chpchtsum  27180  bposlem1  27245  addscan2  27943  slesubaddd  28040  mulscan2dlem  28121  iscgrgd  28438  tgcgr4  28456  lnrot1  28548  eqeelen  28829  nbusgreledg  29278  nb3grprlem2  29306  wspthsnwspthsnon  29844  rusgrnumwwlks  29902  clwwlkwwlksb  29981  clwwlknwwlksnb  29982  dmdmd  32227  nfpconfp  32556  funcnvmpt  32591  1stpreimas  32629  xrdifh  32703  swrdrn3  32877  lsmsnorb  33352  fldextrspunlsp  33661  rhmpreimacnlem  33861  ismntop  34003  eulerpartlemgh  34356  signslema  34540  fmlafvel  35353  topdifinfindis  37310  leceifl  37579  lindsadd  37583  lindsenlbs  37585  iblabsnclem  37653  ftc1anclem6  37668  areacirclem5  37682  areacirc  37683  brcoss3  38397  lsatfixedN  38973  cdlemg10c  40604  diaglbN  41020  dih1  41251  dihglbcpreN  41265  mapdcv  41625  dvdsexpnn0  42330  ef11d  42335  ellz1  42737  islssfg  43041  proot1ex  43167  tfsconcat00  43318  eliooshift  45483  clim2cf  45627  dfatdmfcoafv2  47231  sfprmdvdsmersenne  47565  odd2np1ALTV  47636  vopnbgrelself  47816  rrx2plordisom  48651  i0oii  48842  io1ii  48843  oppccic  48959