Theorem 3bitr2d 310

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr2d.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))
3bitr2d.3	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3bitr2d	⊢ (𝜑 → (𝜓 ↔ 𝜏))

Proof of Theorem 3bitr2d

Step	Hyp	Ref	Expression
1		3bitr2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3bitr2d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	1, 2	bitr4d 285	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 282	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  raltpd  4743  opiota  8044  mapsnend  9021  adderpqlem  10927  mulerpqlem  10928  lesub2  11697  rec11  11904  fimaxre  12150  fiminre  12153  avglt1  12473  ixxun  13379  modmuladdnn0  13942  hashdom  14406  hashle00  14427  hashf1lem1  14482  swrdspsleq  14693  repsdf2  14805  2shfti  15107  mulre  15162  rlim  15536  rlim2  15537  modremain  16456  nn0seqcvgd  16618  divgcdcoprm0  16713  prmreclem6  16971  pwsleval  17537  issubc  17882  ismgmid  18713  grpsubeq0  19083  grpsubadd  19085  eqg0el  19245  gastacos  19371  orbsta  19374  lsslss  21051  prmirredlem  21582  zndvds  21659  zntoslem  21666  cygznlem1  21676  islindf2  21924  ismhp3  22265  coe1mul2lem1  22388  ply1chr  22427  restcld  23290  leordtvallem1  23328  leordtvallem2  23329  ist1-2  23465  xkoccn  23737  qtopcld  23831  ordthmeolem  23919  qustgpopn  24238  isxmet2d  24445  prdsxmetlem  24486  xblss2  24520  imasf1oxms  24607  neibl  24619  xrtgioo  24925  xrsxmet  24928  isncvsngp  25269  minveclem4  25552  minveclem6  25554  minveclem7  25555  mbfmulc2lem  25767  mbfmax  25769  mbfi1fseqlem4  25838  itg2gt0  25880  itg2cnlem2  25882  iblpos  25913  r1pid2  26280  logbgt0b  26916  angrteqvd  26929  affineequiv  26946  affineequiv2  26947  dcubic  26969  rlimcnp  27088  rlimcnp2  27089  efexple  27403  bposlem7  27412  lgsabs1  27458  lgsquadlem1  27502  m1lgs  27510  subadds  28221  lnhl  28842  elplng  29010  colinearalg  29169  axcontlem2  29224  nbupgrel  29604  nb3grpr  29641  usgr0edg0rusgr  29834  isspthonpth  30007  rusgrnumwwlkl1  30229  eupth2lem3lem4  30491  minvecolem4  31141  minvecolem6  31143  minvecolem7  31144  hvmulcan2  31334  xppreima  32902  fzo0opth  33060  fracerl  33542  dvdsrspss  33616  ply1degltel  33801  psrbasfsupp  33818  smatrcl  34103  pstmxmet  34204  xrge0iifcnv  34240  ballotlemsima  34823  poimirlem27  38158  itg2addnclem  38182  itg2addnclem2  38183  iblabsnclem  38194  areacirclem2  38220  areacirclem4  38222  cvlcvrp  39976  ontric3g  44110  alephiso2  44146  sqrtcvallem1  44219  ntrclsk2  44656  ntrclsk13  44659  ntrneixb  44683  neicvgel1  44707  radcnvrat  44888  limsupmnflem  46292  chnsubseqwl  47453  nprmmul1  48131  dfvopnbgr2  48473  pgnbgreunbgrlem2lem1  48734  pgnbgreunbgrlem2lem2  48735  logbge0b  49194  affinecomb2  49334  line2x  49385  itscnhlc0yqe  49390