Theorem 3bitr2d 310

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 285	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 282	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  raltpd  4745  opiota  8060  mapsnend  9047  adderpqlem  10967  mulerpqlem  10968  lesub2  11737  rec11  11941  fimaxre  12187  fiminre  12190  avglt1  12510  ixxun  13418  modmuladdnn0  13983  hashdom  14447  hashle00  14468  hashf1lem1  14524  swrdspsleq  14739  repsdf2  14853  2shfti  15157  mulre  15212  rlim  15586  rlim2  15587  modremain  16504  nn0seqcvgd  16666  divgcdcoprm0  16761  prmreclem6  17019  pwsleval  17585  issubc  17930  ismgmid  18764  grpsubeq0  19155  grpsubadd  19157  eqg0el  19317  gastacos  19443  orbsta  19446  lsslss  21151  prmirredlem  21691  zndvds  21768  zntoslem  21775  cygznlem1  21785  islindf2  22033  ismhp3  22376  coe1mul2lem1  22499  ply1chr  22537  restcld  23403  leordtvallem1  23441  leordtvallem2  23442  ist1-2  23578  xkoccn  23851  qtopcld  23945  ordthmeolem  24033  qustgpopn  24352  isxmet2d  24559  prdsxmetlem  24600  xblss2  24634  imasf1oxms  24721  neibl  24733  xrtgioo  25039  xrsxmet  25042  isncvsngp  25383  minveclem4  25666  minveclem6  25668  minveclem7  25669  mbfmulc2lem  25881  mbfmax  25883  mbfi1fseqlem4  25952  itg2gt0  25994  itg2cnlem2  25996  iblpos  26027  r1pid2  26394  logbgt0b  27038  angrteqvd  27051  affineequiv  27068  affineequiv2  27069  dcubic  27091  rlimcnp  27210  rlimcnp2  27211  efexple  27525  bposlem7  27534  lgsabs1  27580  lgsquadlem1  27624  m1lgs  27632  subadds  28343  lnhl  28968  elplng  29145  colinearalg  29375  axcontlem2  29430  nbupgrel  29813  nb3grpr  29850  usgr0edg0rusgr  30043  isspthonpth  30222  rusgrnumwwlkl1  30447  eupth2lem3lem4  30719  minvecolem4  31369  minvecolem6  31371  minvecolem7  31372  hvmulcan2  31562  xppreima  33126  fzo0opth  33282  fracerl  33755  dvdsrspss  33828  ply1degltel  34012  psrbasfsupp  34029  smatrcl  34314  pstmxmet  34415  xrge0iifcnv  34451  ballotlemsima  35035  poimirlem27  38404  itg2addnclem  38428  itg2addnclem2  38429  iblabsnclem  38440  areacirclem2  38466  areacirclem4  38468  cvlcvrp  40221  ontric3g  44370  alephiso2  44406  sqrtcvallem1  44479  ntrclsk2  44916  ntrclsk13  44919  ntrneixb  44943  neicvgel1  44967  radcnvrat  45146  limsupmnflem  46556  chnsubseqwl  47715  nprmmul1  48435  dfvopnbgr2  48777  pgnbgreunbgrlem2lem1  49038  pgnbgreunbgrlem2lem2  49039  logbge0b  49501  affinecomb2  49641  line2x  49692  itscnhlc0yqe  49697