Theorem 3bitr4rd 311

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  snssgOLD  4788  inimasn  6155  isof1oidb  7320  oacan  8547  ecdmn0  8749  wemapwe  9691  ttrclselem2  9720  r1pw  9839  adderpqlem  10948  mulerpqlem  10949  lterpq  10964  ltanq  10965  genpass  11003  readdcan  11387  lemuldiv  12093  msq11  12114  avglt2  12450  qbtwnre  13177  iooshf  13402  clim2c  15448  lo1o1  15475  climabs0  15528  reef11  16061  absefib  16140  efieq1re  16141  nndivides  16206  oddnn02np1  16290  oddge22np1  16291  evennn02n  16292  evennn2n  16293  halfleoddlt  16304  pc2dvds  16811  pcmpt  16824  subsubc  17802  odmulgid  19421  gexdvds  19451  submcmn2  19706  obslbs  21284  cnntr  22778  cndis  22794  cnindis  22795  cnpdis  22796  lmres  22803  cmpfi  22911  ist0-4  23232  txhmeo  23306  tsmssubm  23646  blin  23926  cncfmet  24424  icopnfcnv  24457  lmmbrf  24778  iscauf  24796  causs  24814  mbfposr  25168  itg2gt0  25277  limcflf  25397  limcres  25402  lhop1  25530  dvdsr1p  25678  fsumvma2  26714  vmasum  26716  chpchtsum  26719  bposlem1  26784  addscan2  27473  mulscan2dlem  27627  iscgrgd  27761  tgcgr4  27779  lnrot1  27871  eqeelen  28159  nbusgreledg  28607  nb3grprlem2  28635  wspthsnwspthsnon  29167  rusgrnumwwlks  29225  clwwlkwwlksb  29304  clwwlknwwlksnb  29305  dmdmd  31548  nfpconfp  31851  funcnvmpt  31887  1stpreimas  31922  xrdifh  31986  swrdrn3  32114  lsmsnorb  32496  ghmqusker  32527  rhmpreimacnlem  32859  ismntop  33001  eulerpartlemgh  33372  signslema  33568  fmlafvel  34371  topdifinfindis  36222  leceifl  36472  lindsadd  36476  lindsenlbs  36478  iblabsnclem  36546  ftc1anclem6  36561  areacirclem5  36575  areacirc  36576  brcoss3  37298  lsatfixedN  37874  cdlemg10c  39505  diaglbN  39921  dih1  40152  dihglbcpreN  40166  mapdcv  40526  dvdsexpnn0  41232  ellz1  41495  islssfg  41802  proot1ex  41933  tfsconcat00  42087  eliooshift  44209  clim2cf  44356  dfatdmfcoafv2  45952  sfprmdvdsmersenne  46261  odd2np1ALTV  46332  rrx2plordisom  47399  i0oii  47542  io1ii  47543