Theorem 3bitr4rd 314

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  snssg  4717  inimasn  6013  isof1oidb  7077  oacan  8174  ecdmn0  8336  wemapwe  9160  r1pw  9274  adderpqlem  10376  mulerpqlem  10377  lterpq  10392  ltanq  10393  genpass  10431  readdcan  10814  lemuldiv  11520  msq11  11541  avglt2  11877  qbtwnre  12593  iooshf  12816  clim2c  14862  lo1o1  14889  climabs0  14942  reef11  15472  absefib  15551  efieq1re  15552  nndivides  15617  oddnn02np1  15697  oddge22np1  15698  evennn02n  15699  evennn2n  15700  halfleoddlt  15711  pc2dvds  16215  pcmpt  16228  subsubc  17123  odmulgid  18681  gexdvds  18709  submcmn2  18959  obslbs  20874  cnntr  21883  cndis  21899  cnindis  21900  cnpdis  21901  lmres  21908  cmpfi  22016  ist0-4  22337  txhmeo  22411  tsmssubm  22751  blin  23031  cncfmet  23516  icopnfcnv  23546  lmmbrf  23865  iscauf  23883  causs  23901  mbfposr  24253  itg2gt0  24361  limcflf  24479  limcres  24484  lhop1  24611  dvdsr1p  24755  fsumvma2  25790  vmasum  25792  chpchtsum  25795  bposlem1  25860  iscgrgd  26299  tgcgr4  26317  lnrot1  26409  eqeelen  26690  nbusgreledg  27135  nb3grprlem2  27163  wspthsnwspthsnon  27695  rusgrnumwwlks  27753  clwwlkwwlksb  27833  clwwlknwwlksnb  27834  dmdmd  30077  nfpconfp  30377  funcnvmpt  30412  1stpreimas  30441  xrdifh  30503  swrdrn3  30629  lsmsnorb  30945  ismntop  31267  eulerpartlemgh  31636  signslema  31832  fmlafvel  32632  topdifinfindis  34630  leceifl  34896  lindsadd  34900  lindsenlbs  34902  iblabsnclem  34970  ftc1anclem6  34987  areacirclem5  35001  areacirc  35002  brcoss3  35693  lsatfixedN  36160  cdlemg10c  37790  diaglbN  38206  dih1  38437  dihglbcpreN  38451  mapdcv  38811  ellz1  39413  islssfg  39719  proot1ex  39850  eliooshift  41831  clim2cf  41980  dfatdmfcoafv2  43502  sfprmdvdsmersenne  43817  odd2np1ALTV  43888  rrx2plordisom  44759