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  4745  opiota  8038  mapsnend  9007  adderpqlem  10907  mulerpqlem  10908  lesub2  11673  rec11  11880  fimaxre  12127  fiminre  12130  avglt1  12420  ixxun  13322  modmuladdnn0  13880  hashdom  14344  hashle00  14365  hashf1lem1  14420  swrdspsleq  14630  repsdf2  14743  2shfti  15046  mulre  15087  rlim  15461  rlim2  15462  modremain  16378  nn0seqcvgd  16540  divgcdcoprm0  16635  prmreclem6  16892  pwsleval  17456  issubc  17797  ismgmid  18592  grpsubeq0  18958  grpsubadd  18960  eqg0el  19115  gastacos  19242  orbsta  19245  lsslss  20867  prmirredlem  21382  zndvds  21459  zntoslem  21466  cygznlem1  21476  islindf2  21723  ismhp3  22029  coe1mul2lem1  22153  ply1chr  22193  restcld  23059  leordtvallem1  23097  leordtvallem2  23098  ist1-2  23234  xkoccn  23506  qtopcld  23600  ordthmeolem  23688  qustgpopn  24007  isxmet2d  24215  prdsxmetlem  24256  xblss2  24290  imasf1oxms  24377  neibl  24389  xrtgioo  24695  xrsxmet  24698  isncvsngp  25049  minveclem4  25332  minveclem6  25334  minveclem7  25335  mbfmulc2lem  25548  mbfmax  25550  mbfi1fseqlem4  25619  itg2gt0  25661  itg2cnlem2  25663  iblpos  25694  r1pid2  26067  logbgt0b  26703  angrteqvd  26716  affineequiv  26733  affineequiv2  26734  dcubic  26756  rlimcnp  26875  rlimcnp2  26876  efexple  27192  bposlem7  27201  lgsabs1  27247  lgsquadlem1  27291  m1lgs  27299  subadds  27974  lnhl  28542  colinearalg  28837  axcontlem2  28892  nbupgrel  29272  nb3grpr  29309  usgr0edg0rusgr  29503  isspthonpth  29679  rusgrnumwwlkl1  29898  eupth2lem3lem4  30160  minvecolem4  30809  minvecolem6  30811  minvecolem7  30812  hvmulcan2  31002  xppreima  32569  fzo0opth  32728  fracerl  33256  dvdsrspss  33358  ply1degltel  33560  r1pid2OLD  33574  smatrcl  33786  pstmxmet  33887  xrge0iifcnv  33923  ballotlemsima  34507  poimirlem27  37641  itg2addnclem  37665  itg2addnclem2  37666  iblabsnclem  37677  areacirclem2  37703  areacirclem4  37705  cvlcvrp  39333  ontric3g  43511  alephiso2  43547  sqrtcvallem1  43620  ntrclsk2  44057  ntrclsk13  44060  ntrneixb  44084  neicvgel1  44108  radcnvrat  44303  limsupmnflem  45718  dfvopnbgr2  47853  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  logbge0b  48552  affinecomb2  48692  line2x  48743  itscnhlc0yqe  48748