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  6114  isof1oidb  7270  oacan  8475  ecdmn0  8687  wemapwe  9606  ttrclselem2  9635  r1pw  9757  adderpqlem  10865  mulerpqlem  10866  lterpq  10881  ltanq  10882  genpass  10920  readdcan  11307  lemuldiv  12022  msq11  12043  avglt2  12380  qbtwnre  13114  iooshf  13342  clim2c  15428  lo1o1  15455  climabs0  15508  reef11  16044  absefib  16123  efieq1re  16124  nndivides  16189  oddnn02np1  16275  oddge22np1  16276  evennn02n  16277  evennn2n  16278  halfleoddlt  16289  pc2dvds  16807  pcmpt  16820  subsubc  17777  ghmqusker  19216  odmulgid  19483  gexdvds  19513  submcmn2  19768  obslbs  21685  cnntr  23219  cndis  23235  cnindis  23236  cnpdis  23237  lmres  23244  cmpfi  23352  ist0-4  23673  txhmeo  23747  tsmssubm  24087  blin  24365  cncfmet  24858  icopnfcnv  24896  lmmbrf  25218  iscauf  25236  causs  25254  mbfposr  25609  itg2gt0  25717  limcflf  25838  limcres  25843  lhop1  25975  dvdsr1p  26125  fsumvma2  27181  vmasum  27183  chpchtsum  27186  bposlem1  27251  addscan2  27989  lesubaddsd  28089  mulscan2dlem  28174  bdayfinbndlem1  28463  iscgrgd  28585  tgcgr4  28603  lnrot1  28695  eqeelen  28977  nbusgreledg  29426  nb3grprlem2  29454  wspthsnwspthsnon  29989  rusgrnumwwlks  30050  clwwlkwwlksb  30129  clwwlknwwlksnb  30130  dmdmd  32375  nfpconfp  32710  funcnvmpt  32745  1stpreimas  32785  xrdifh  32860  swrdrn3  33037  lsmsnorb  33472  fldextrspunlsp  33831  rhmpreimacnlem  34041  ismntop  34183  eulerpartlemgh  34535  signslema  34719  fmlafvel  35579  topdifinfindis  37551  leceifl  37810  lindsadd  37814  lindsenlbs  37816  iblabsnclem  37884  ftc1anclem6  37899  areacirclem5  37913  areacirc  37914  brcoss3  38696  lsatfixedN  39269  cdlemg10c  40899  diaglbN  41315  dih1  41546  dihglbcpreN  41560  mapdcv  41920  dvdsexpnn0  42589  ef11d  42594  ellz1  43009  islssfg  43312  proot1ex  43438  tfsconcat00  43589  eliooshift  45752  clim2cf  45894  dfatdmfcoafv2  47500  sfprmdvdsmersenne  47849  odd2np1ALTV  47920  vopnbgrelself  48101  rrx2plordisom  48969  i0oii  49165  io1ii  49166  oppccic  49289  uptrlem3  49457  uptr2  49466