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  4734  opiota  7991  mapsnend  8958  adderpqlem  10842  mulerpqlem  10843  lesub2  11609  rec11  11816  fimaxre  12063  fiminre  12066  avglt1  12356  ixxun  13258  modmuladdnn0  13819  hashdom  14283  hashle00  14304  hashf1lem1  14359  swrdspsleq  14570  repsdf2  14682  2shfti  14984  mulre  15025  rlim  15399  rlim2  15400  modremain  16316  nn0seqcvgd  16478  divgcdcoprm0  16573  prmreclem6  16830  pwsleval  17394  issubc  17739  ismgmid  18570  grpsubeq0  18936  grpsubadd  18938  eqg0el  19093  gastacos  19220  orbsta  19223  lsslss  20892  prmirredlem  21407  zndvds  21484  zntoslem  21491  cygznlem1  21501  islindf2  21749  ismhp3  22055  coe1mul2lem1  22179  ply1chr  22219  restcld  23085  leordtvallem1  23123  leordtvallem2  23124  ist1-2  23260  xkoccn  23532  qtopcld  23626  ordthmeolem  23714  qustgpopn  24033  isxmet2d  24240  prdsxmetlem  24281  xblss2  24315  imasf1oxms  24402  neibl  24414  xrtgioo  24720  xrsxmet  24723  isncvsngp  25074  minveclem4  25357  minveclem6  25359  minveclem7  25360  mbfmulc2lem  25573  mbfmax  25575  mbfi1fseqlem4  25644  itg2gt0  25686  itg2cnlem2  25688  iblpos  25719  r1pid2  26092  logbgt0b  26728  angrteqvd  26741  affineequiv  26758  affineequiv2  26759  dcubic  26781  rlimcnp  26900  rlimcnp2  26901  efexple  27217  bposlem7  27226  lgsabs1  27272  lgsquadlem1  27316  m1lgs  27324  subadds  28008  lnhl  28591  colinearalg  28886  axcontlem2  28941  nbupgrel  29321  nb3grpr  29358  usgr0edg0rusgr  29552  isspthonpth  29725  rusgrnumwwlkl1  29944  eupth2lem3lem4  30206  minvecolem4  30855  minvecolem6  30857  minvecolem7  30858  hvmulcan2  31048  xppreima  32622  fzo0opth  32780  fracerl  33267  dvdsrspss  33347  ply1degltel  33550  r1pid2OLD  33564  psrbasfsupp  33567  smatrcl  33804  pstmxmet  33905  xrge0iifcnv  33941  ballotlemsima  34524  poimirlem27  37686  itg2addnclem  37710  itg2addnclem2  37711  iblabsnclem  37722  areacirclem2  37748  areacirclem4  37750  cvlcvrp  39378  ontric3g  43554  alephiso2  43590  sqrtcvallem1  43663  ntrclsk2  44100  ntrclsk13  44103  ntrneixb  44127  neicvgel1  44151  radcnvrat  44346  limsupmnflem  45757  dfvopnbgr2  47883  pgnbgreunbgrlem2lem1  48144  pgnbgreunbgrlem2lem2  48145  logbge0b  48594  affinecomb2  48734  line2x  48785  itscnhlc0yqe  48790