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  4788  inimasn  6177  isof1oidb  7343  oacan  8584  ecdmn0  8792  wemapwe  9734  ttrclselem2  9763  r1pw  9882  adderpqlem  10991  mulerpqlem  10992  lterpq  11007  ltanq  11008  genpass  11046  readdcan  11432  lemuldiv  12145  msq11  12166  avglt2  12502  qbtwnre  13237  iooshf  13462  clim2c  15537  lo1o1  15564  climabs0  15617  reef11  16151  absefib  16230  efieq1re  16231  nndivides  16296  oddnn02np1  16381  oddge22np1  16382  evennn02n  16383  evennn2n  16384  halfleoddlt  16395  pc2dvds  16912  pcmpt  16925  subsubc  17903  ghmqusker  19317  odmulgid  19586  gexdvds  19616  submcmn2  19871  obslbs  21767  cnntr  23298  cndis  23314  cnindis  23315  cnpdis  23316  lmres  23323  cmpfi  23431  ist0-4  23752  txhmeo  23826  tsmssubm  24166  blin  24446  cncfmet  24948  icopnfcnv  24986  lmmbrf  25309  iscauf  25327  causs  25345  mbfposr  25700  itg2gt0  25809  limcflf  25930  limcres  25935  lhop1  26067  dvdsr1p  26217  fsumvma2  27272  vmasum  27274  chpchtsum  27277  bposlem1  27342  addscan2  28040  slesubaddd  28137  mulscan2dlem  28218  iscgrgd  28535  tgcgr4  28553  lnrot1  28645  eqeelen  28933  nbusgreledg  29384  nb3grprlem2  29412  wspthsnwspthsnon  29945  rusgrnumwwlks  30003  clwwlkwwlksb  30082  clwwlknwwlksnb  30083  dmdmd  32328  nfpconfp  32648  funcnvmpt  32683  1stpreimas  32720  xrdifh  32788  swrdrn3  32924  lsmsnorb  33398  rhmpreimacnlem  33844  ismntop  33988  eulerpartlemgh  34359  signslema  34555  fmlafvel  35369  topdifinfindis  37328  leceifl  37595  lindsadd  37599  lindsenlbs  37601  iblabsnclem  37669  ftc1anclem6  37684  areacirclem5  37698  areacirc  37699  brcoss3  38414  lsatfixedN  38990  cdlemg10c  40621  diaglbN  41037  dih1  41268  dihglbcpreN  41282  mapdcv  41642  dvdsexpnn0  42347  ef11d  42353  ellz1  42754  islssfg  43058  proot1ex  43184  tfsconcat00  43336  eliooshift  45458  clim2cf  45605  dfatdmfcoafv2  47203  sfprmdvdsmersenne  47527  odd2np1ALTV  47598  vopnbgrelself  47778  rrx2plordisom  48572  i0oii  48715  io1ii  48716