Theorem 3bitr2d 308

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  raltpd  4720  opiota  8008  mapsnend  8980  adderpqlem  10875  mulerpqlem  10876  lesub2  11643  rec11  11851  fimaxre  12098  fiminre  12101  avglt1  12413  ixxun  13312  modmuladdnn0  13875  hashdom  14339  hashle00  14360  hashf1lem1  14415  swrdspsleq  14626  repsdf2  14738  2shfti  15040  mulre  15081  rlim  15455  rlim2  15456  modremain  16375  nn0seqcvgd  16537  divgcdcoprm0  16632  prmreclem6  16890  pwsleval  17455  issubc  17800  ismgmid  18631  grpsubeq0  19000  grpsubadd  19002  eqg0el  19156  gastacos  19283  orbsta  19286  lsslss  20958  prmirredlem  21454  zndvds  21531  zntoslem  21538  cygznlem1  21548  islindf2  21796  ismhp3  22137  coe1mul2lem1  22260  ply1chr  22299  restcld  23162  leordtvallem1  23200  leordtvallem2  23201  ist1-2  23337  xkoccn  23609  qtopcld  23703  ordthmeolem  23791  qustgpopn  24110  isxmet2d  24317  prdsxmetlem  24358  xblss2  24392  imasf1oxms  24479  neibl  24491  xrtgioo  24797  xrsxmet  24800  isncvsngp  25141  minveclem4  25424  minveclem6  25426  minveclem7  25427  mbfmulc2lem  25639  mbfmax  25641  mbfi1fseqlem4  25710  itg2gt0  25752  itg2cnlem2  25754  iblpos  25785  r1pid2  26152  logbgt0b  26782  angrteqvd  26795  affineequiv  26812  affineequiv2  26813  dcubic  26835  rlimcnp  26954  rlimcnp2  26955  efexple  27269  bposlem7  27278  lgsabs1  27324  lgsquadlem1  27368  m1lgs  27376  subadds  28087  lnhl  28708  colinearalg  29004  axcontlem2  29059  nbupgrel  29439  nb3grpr  29476  usgr0edg0rusgr  29669  isspthonpth  29842  rusgrnumwwlkl1  30064  eupth2lem3lem4  30326  minvecolem4  30976  minvecolem6  30978  minvecolem7  30979  hvmulcan2  31169  xppreima  32744  fzo0opth  32902  fracerl  33397  dvdsrspss  33477  ply1degltel  33684  r1pid2OLD  33699  psrbasfsupp  33702  smatrcl  33987  pstmxmet  34088  xrge0iifcnv  34124  ballotlemsima  34707  poimirlem27  38021  itg2addnclem  38045  itg2addnclem2  38046  iblabsnclem  38057  areacirclem2  38083  areacirclem4  38085  cvlcvrp  39839  ontric3g  43973  alephiso2  44009  sqrtcvallem1  44082  ntrclsk2  44519  ntrclsk13  44522  ntrneixb  44546  neicvgel1  44570  radcnvrat  44765  limsupmnflem  46170  chnsubseqwl  47331  nprmmul1  48009  dfvopnbgr2  48351  pgnbgreunbgrlem2lem1  48612  pgnbgreunbgrlem2lem2  48613  logbge0b  49061  affinecomb2  49201  line2x  49252  itscnhlc0yqe  49257