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 ⊢ (𝜑 → (𝜏 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  inimasn  6155  funcnvmpt  6995  isof1oidb  7328  oacan  8535  ecdmn0  8749  wemapwe  9669  ttrclselem2  9698  r1pw  9820  adderpqlem  10950  mulerpqlem  10951  lterpq  10966  ltanq  10967  genpass  11005  readdcan  11395  lemuldiv  12106  msq11  12127  avglt2  12494  qbtwnre  13236  iooshf  13464  swrdrn3  14707  clim2c  15575  lo1o1  15602  climabs0  15655  reef11  16192  absefib  16271  efieq1re  16272  nndivides  16337  oddnn02np1  16423  oddge22np1  16424  evennn02n  16425  evennn2n  16426  halfleoddlt  16437  pc2dvds  16956  pcmpt  16969  subsubc  17927  ghmqusker  19380  odmulgid  19647  gexdvds  19677  submcmn2  19932  obslbs  21909  cnntr  23461  cndis  23477  cnindis  23478  cnpdis  23479  lmres  23486  cmpfi  23594  ist0-4  23915  txhmeo  23989  tsmssubm  24329  blin  24607  cncfmet  25097  icopnfcnv  25130  lmmbrf  25450  iscauf  25468  causs  25486  mbfposr  25840  itg2gt0  25948  limcflf  26069  limcres  26074  lhop1  26202  dvdsr1p  26350  fsumvma2  27407  vmasum  27409  chpchtsum  27412  bposlem1  27477  addscan2  28215  lesubaddsd  28315  mulscan2dlem  28400  bdayfinbndlem1  28689  iscgrgd  28811  tgcgr4  28829  lnrot1  28925  dfprlng2  29226  eqeelen  29283  nbusgreledg  29732  nb3grprlem2  29760  wspthsnwspthsnon  30294  rusgrnumwwlks  30355  clwwlkwwlksb  30434  clwwlknwwlksnb  30435  dmdmd  32681  nfpconfp  33006  1stpreimas  33080  xrdifh  33154  lsmsnorb  33727  esplyfval1  33986  fldextrspunlsp  34087  rhmpreimacnlem  34297  ismntop  34439  eulerpartlemgh  34792  signslema  34973  fmlafvel  35890  topdifinfindis  38025  leceifl  38293  lindsadd  38297  lindsenlbs  38299  iblabsnclem  38367  ftc1anclem6  38382  areacirclem5  38396  areacirc  38397  brcoss3  39205  lsatfixedN  39816  cdlemg10c  41446  diaglbN  41862  dih1  42093  dihglbcpreN  42107  mapdcv  42467  dvdsexpnn0  43128  ef11d  43133  ellz1  43531  islssfg  43830  proot1ex  43956  tfsconcat00  44107  eliooshift  46255  clim2cf  46397  dfatdmfcoafv2  48024  sfprmdvdsmersenne  48388  odd2np1ALTV  48472  vopnbgrelself  48653  rrx2plordisom  49536  i0oii  49731  io1ii  49732  oppccic  49855  uptrlem3  50023  uptr2  50032