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  4733  opiota  7997  mapsnend  8965  adderpqlem  10852  mulerpqlem  10853  lesub2  11619  rec11  11826  fimaxre  12073  fiminre  12076  avglt1  12366  ixxun  13263  modmuladdnn0  13824  hashdom  14288  hashle00  14309  hashf1lem1  14364  swrdspsleq  14575  repsdf2  14687  2shfti  14989  mulre  15030  rlim  15404  rlim2  15405  modremain  16321  nn0seqcvgd  16483  divgcdcoprm0  16578  prmreclem6  16835  pwsleval  17399  issubc  17744  ismgmid  18575  grpsubeq0  18941  grpsubadd  18943  eqg0el  19097  gastacos  19224  orbsta  19227  lsslss  20896  prmirredlem  21411  zndvds  21488  zntoslem  21495  cygznlem1  21505  islindf2  21753  ismhp3  22058  coe1mul2lem1  22182  ply1chr  22222  restcld  23088  leordtvallem1  23126  leordtvallem2  23127  ist1-2  23263  xkoccn  23535  qtopcld  23629  ordthmeolem  23717  qustgpopn  24036  isxmet2d  24243  prdsxmetlem  24284  xblss2  24318  imasf1oxms  24405  neibl  24417  xrtgioo  24723  xrsxmet  24726  isncvsngp  25077  minveclem4  25360  minveclem6  25362  minveclem7  25363  mbfmulc2lem  25576  mbfmax  25578  mbfi1fseqlem4  25647  itg2gt0  25689  itg2cnlem2  25691  iblpos  25722  r1pid2  26095  logbgt0b  26731  angrteqvd  26744  affineequiv  26761  affineequiv2  26762  dcubic  26784  rlimcnp  26903  rlimcnp2  26904  efexple  27220  bposlem7  27229  lgsabs1  27275  lgsquadlem1  27319  m1lgs  27327  subadds  28011  lnhl  28594  colinearalg  28890  axcontlem2  28945  nbupgrel  29325  nb3grpr  29362  usgr0edg0rusgr  29556  isspthonpth  29729  rusgrnumwwlkl1  29951  eupth2lem3lem4  30213  minvecolem4  30862  minvecolem6  30864  minvecolem7  30865  hvmulcan2  31055  xppreima  32629  fzo0opth  32790  fracerl  33279  dvdsrspss  33359  ply1degltel  33562  r1pid2OLD  33576  psrbasfsupp  33579  smatrcl  33830  pstmxmet  33931  xrge0iifcnv  33967  ballotlemsima  34550  poimirlem27  37707  itg2addnclem  37731  itg2addnclem2  37732  iblabsnclem  37743  areacirclem2  37769  areacirclem4  37771  cvlcvrp  39459  ontric3g  43639  alephiso2  43675  sqrtcvallem1  43748  ntrclsk2  44185  ntrclsk13  44188  ntrneixb  44212  neicvgel1  44236  radcnvrat  44431  limsupmnflem  45842  chnsubseqwl  47001  dfvopnbgr2  47977  pgnbgreunbgrlem2lem1  48238  pgnbgreunbgrlem2lem2  48239  logbge0b  48688  affinecomb2  48828  line2x  48879  itscnhlc0yqe  48884