Theorem 3bitr2d 307

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 282	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 279	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:  raltpd  4735  opiota  8001  mapsnend  8968  adderpqlem  10867  mulerpqlem  10868  lesub2  11633  rec11  11840  fimaxre  12087  fiminre  12090  avglt1  12380  ixxun  13282  modmuladdnn0  13840  hashdom  14304  hashle00  14325  hashf1lem1  14380  swrdspsleq  14590  repsdf2  14702  2shfti  15005  mulre  15046  rlim  15420  rlim2  15421  modremain  16337  nn0seqcvgd  16499  divgcdcoprm0  16594  prmreclem6  16851  pwsleval  17415  issubc  17760  ismgmid  18557  grpsubeq0  18923  grpsubadd  18925  eqg0el  19080  gastacos  19207  orbsta  19210  lsslss  20882  prmirredlem  21397  zndvds  21474  zntoslem  21481  cygznlem1  21491  islindf2  21739  ismhp3  22045  coe1mul2lem1  22169  ply1chr  22209  restcld  23075  leordtvallem1  23113  leordtvallem2  23114  ist1-2  23250  xkoccn  23522  qtopcld  23616  ordthmeolem  23704  qustgpopn  24023  isxmet2d  24231  prdsxmetlem  24272  xblss2  24306  imasf1oxms  24393  neibl  24405  xrtgioo  24711  xrsxmet  24714  isncvsngp  25065  minveclem4  25348  minveclem6  25350  minveclem7  25351  mbfmulc2lem  25564  mbfmax  25566  mbfi1fseqlem4  25635  itg2gt0  25677  itg2cnlem2  25679  iblpos  25710  r1pid2  26083  logbgt0b  26719  angrteqvd  26732  affineequiv  26749  affineequiv2  26750  dcubic  26772  rlimcnp  26891  rlimcnp2  26892  efexple  27208  bposlem7  27217  lgsabs1  27263  lgsquadlem1  27307  m1lgs  27315  subadds  27997  lnhl  28578  colinearalg  28873  axcontlem2  28928  nbupgrel  29308  nb3grpr  29345  usgr0edg0rusgr  29539  isspthonpth  29712  rusgrnumwwlkl1  29931  eupth2lem3lem4  30193  minvecolem4  30842  minvecolem6  30844  minvecolem7  30845  hvmulcan2  31035  xppreima  32602  fzo0opth  32761  fracerl  33255  dvdsrspss  33334  ply1degltel  33536  r1pid2OLD  33550  smatrcl  33762  pstmxmet  33863  xrge0iifcnv  33899  ballotlemsima  34483  poimirlem27  37626  itg2addnclem  37650  itg2addnclem2  37651  iblabsnclem  37662  areacirclem2  37688  areacirclem4  37690  cvlcvrp  39318  ontric3g  43495  alephiso2  43531  sqrtcvallem1  43604  ntrclsk2  44041  ntrclsk13  44044  ntrneixb  44068  neicvgel1  44092  radcnvrat  44287  limsupmnflem  45702  dfvopnbgr2  47838  pgnbgreunbgrlem2lem1  48099  pgnbgreunbgrlem2lem2  48100  logbge0b  48549  affinecomb2  48689  line2x  48740  itscnhlc0yqe  48745