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  4781  opiota  8084  mapsnend  9076  adderpqlem  10994  mulerpqlem  10995  lesub2  11758  rec11  11965  fimaxre  12212  fiminre  12215  avglt1  12504  ixxun  13403  modmuladdnn0  13956  hashdom  14418  hashle00  14439  hashf1lem1  14494  swrdspsleq  14703  repsdf2  14816  2shfti  15119  mulre  15160  rlim  15531  rlim2  15532  modremain  16445  nn0seqcvgd  16607  divgcdcoprm0  16702  prmreclem6  16959  pwsleval  17538  issubc  17880  ismgmid  18678  grpsubeq0  19044  grpsubadd  19046  eqg0el  19201  gastacos  19328  orbsta  19331  lsslss  20959  prmirredlem  21483  zndvds  21568  zntoslem  21575  cygznlem1  21585  islindf2  21834  ismhp3  22146  coe1mul2lem1  22270  ply1chr  22310  restcld  23180  leordtvallem1  23218  leordtvallem2  23219  ist1-2  23355  xkoccn  23627  qtopcld  23721  ordthmeolem  23809  qustgpopn  24128  isxmet2d  24337  prdsxmetlem  24378  xblss2  24412  imasf1oxms  24502  neibl  24514  xrtgioo  24828  xrsxmet  24831  isncvsngp  25183  minveclem4  25466  minveclem6  25468  minveclem7  25469  mbfmulc2lem  25682  mbfmax  25684  mbfi1fseqlem4  25753  itg2gt0  25795  itg2cnlem2  25797  iblpos  25828  r1pid2  26201  logbgt0b  26836  angrteqvd  26849  affineequiv  26866  affineequiv2  26867  dcubic  26889  rlimcnp  27008  rlimcnp2  27009  efexple  27325  bposlem7  27334  lgsabs1  27380  lgsquadlem1  27424  m1lgs  27432  subadds  28100  lnhl  28623  colinearalg  28925  axcontlem2  28980  nbupgrel  29362  nb3grpr  29399  usgr0edg0rusgr  29593  isspthonpth  29769  rusgrnumwwlkl1  29988  eupth2lem3lem4  30250  minvecolem4  30899  minvecolem6  30901  minvecolem7  30902  hvmulcan2  31092  xppreima  32655  fzo0opth  32807  fracerl  33308  dvdsrspss  33415  ply1degltel  33615  r1pid2OLD  33629  smatrcl  33795  pstmxmet  33896  xrge0iifcnv  33932  ballotlemsima  34518  poimirlem27  37654  itg2addnclem  37678  itg2addnclem2  37679  iblabsnclem  37690  areacirclem2  37716  areacirclem4  37718  cvlcvrp  39341  ontric3g  43535  alephiso2  43571  sqrtcvallem1  43644  ntrclsk2  44081  ntrclsk13  44084  ntrneixb  44108  neicvgel1  44132  radcnvrat  44333  limsupmnflem  45735  dfvopnbgr2  47839  logbge0b  48484  affinecomb2  48624  line2x  48675  itscnhlc0yqe  48680