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  4748  opiota  8057  mapsnend  9034  adderpqlem  10940  mulerpqlem  10941  lesub2  11710  rec11  11914  fimaxre  12160  fiminre  12163  avglt1  12483  ixxun  13389  modmuladdnn0  13953  hashdom  14417  hashle00  14438  hashf1lem1  14494  swrdspsleq  14705  repsdf2  14817  2shfti  15119  mulre  15174  rlim  15548  rlim2  15549  modremain  16467  nn0seqcvgd  16629  divgcdcoprm0  16724  prmreclem6  16982  pwsleval  17548  issubc  17893  ismgmid  18724  grpsubeq0  19093  grpsubadd  19095  eqg0el  19255  gastacos  19381  orbsta  19384  lsslss  21063  prmirredlem  21603  zndvds  21680  zntoslem  21687  cygznlem1  21697  islindf2  21945  ismhp3  22286  coe1mul2lem1  22409  ply1chr  22447  restcld  23310  leordtvallem1  23348  leordtvallem2  23349  ist1-2  23485  xkoccn  23757  qtopcld  23851  ordthmeolem  23939  qustgpopn  24258  isxmet2d  24465  prdsxmetlem  24506  xblss2  24540  imasf1oxms  24627  neibl  24639  xrtgioo  24945  xrsxmet  24948  isncvsngp  25289  minveclem4  25572  minveclem6  25574  minveclem7  25575  mbfmulc2lem  25787  mbfmax  25789  mbfi1fseqlem4  25858  itg2gt0  25900  itg2cnlem2  25902  iblpos  25933  r1pid2  26300  logbgt0b  26936  angrteqvd  26949  affineequiv  26966  affineequiv2  26967  dcubic  26989  rlimcnp  27108  rlimcnp2  27109  efexple  27423  bposlem7  27432  lgsabs1  27478  lgsquadlem1  27522  m1lgs  27530  subadds  28241  lnhl  28865  elplng  29040  colinearalg  29238  axcontlem2  29293  nbupgrel  29673  nb3grpr  29710  usgr0edg0rusgr  29903  isspthonpth  30076  rusgrnumwwlkl1  30298  eupth2lem3lem4  30560  minvecolem4  31210  minvecolem6  31212  minvecolem7  31213  hvmulcan2  31403  xppreima  32968  fzo0opth  33126  fracerl  33605  dvdsrspss  33678  ply1degltel  33862  psrbasfsupp  33879  smatrcl  34164  pstmxmet  34265  xrge0iifcnv  34301  ballotlemsima  34884  poimirlem27  38276  itg2addnclem  38300  itg2addnclem2  38301  iblabsnclem  38312  areacirclem2  38338  areacirclem4  38340  cvlcvrp  40092  ontric3g  44228  alephiso2  44264  sqrtcvallem1  44337  ntrclsk2  44774  ntrclsk13  44777  ntrneixb  44801  neicvgel1  44825  radcnvrat  45004  limsupmnflem  46414  chnsubseqwl  47575  nprmmul1  48253  dfvopnbgr2  48595  pgnbgreunbgrlem2lem1  48856  pgnbgreunbgrlem2lem2  48857  logbge0b  49320  affinecomb2  49460  line2x  49511  itscnhlc0yqe  49516