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  4738  opiota  8003  mapsnend  8973  adderpqlem  10865  mulerpqlem  10866  lesub2  11632  rec11  11839  fimaxre  12086  fiminre  12089  avglt1  12379  ixxun  13277  modmuladdnn0  13838  hashdom  14302  hashle00  14323  hashf1lem1  14378  swrdspsleq  14589  repsdf2  14701  2shfti  15003  mulre  15044  rlim  15418  rlim2  15419  modremain  16335  nn0seqcvgd  16497  divgcdcoprm0  16592  prmreclem6  16849  pwsleval  17414  issubc  17759  ismgmid  18590  grpsubeq0  18956  grpsubadd  18958  eqg0el  19112  gastacos  19239  orbsta  19242  lsslss  20912  prmirredlem  21427  zndvds  21504  zntoslem  21511  cygznlem1  21521  islindf2  21769  ismhp3  22085  coe1mul2lem1  22209  ply1chr  22250  restcld  23116  leordtvallem1  23154  leordtvallem2  23155  ist1-2  23291  xkoccn  23563  qtopcld  23657  ordthmeolem  23745  qustgpopn  24064  isxmet2d  24271  prdsxmetlem  24312  xblss2  24346  imasf1oxms  24433  neibl  24445  xrtgioo  24751  xrsxmet  24754  isncvsngp  25105  minveclem4  25388  minveclem6  25390  minveclem7  25391  mbfmulc2lem  25604  mbfmax  25606  mbfi1fseqlem4  25675  itg2gt0  25717  itg2cnlem2  25719  iblpos  25750  r1pid2  26123  logbgt0b  26759  angrteqvd  26772  affineequiv  26789  affineequiv2  26790  dcubic  26812  rlimcnp  26931  rlimcnp2  26932  efexple  27248  bposlem7  27257  lgsabs1  27303  lgsquadlem1  27347  m1lgs  27355  subadds  28066  lnhl  28687  colinearalg  28983  axcontlem2  29038  nbupgrel  29418  nb3grpr  29455  usgr0edg0rusgr  29649  isspthonpth  29822  rusgrnumwwlkl1  30044  eupth2lem3lem4  30306  minvecolem4  30955  minvecolem6  30957  minvecolem7  30958  hvmulcan2  31148  xppreima  32723  fzo0opth  32883  fracerl  33388  dvdsrspss  33468  ply1degltel  33675  r1pid2OLD  33690  psrbasfsupp  33693  smatrcl  33953  pstmxmet  34054  xrge0iifcnv  34090  ballotlemsima  34673  poimirlem27  37844  itg2addnclem  37868  itg2addnclem2  37869  iblabsnclem  37880  areacirclem2  37906  areacirclem4  37908  cvlcvrp  39596  ontric3g  43759  alephiso2  43795  sqrtcvallem1  43868  ntrclsk2  44305  ntrclsk13  44308  ntrneixb  44332  neicvgel1  44356  radcnvrat  44551  limsupmnflem  45960  chnsubseqwl  47119  dfvopnbgr2  48095  pgnbgreunbgrlem2lem1  48356  pgnbgreunbgrlem2lem2  48357  logbge0b  48805  affinecomb2  48945  line2x  48996  itscnhlc0yqe  49001