Theorem 3bitr2d 306

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  raltpd  4780  opiota  8065  mapsnend  9064  adderpqlem  10988  mulerpqlem  10989  lesub2  11750  rec11  11957  fimaxre  12204  fiminre  12207  avglt1  12496  ixxun  13388  modmuladdnn0  13929  hashdom  14391  hashle00  14412  hashf1lem1  14468  hashf1lem1OLD  14469  swrdspsleq  14668  repsdf2  14781  2shfti  15080  mulre  15121  rlim  15492  rlim2  15493  modremain  16405  nn0seqcvgd  16566  divgcdcoprm0  16661  prmreclem6  16918  pwsleval  17503  issubc  17849  ismgmid  18653  grpsubeq0  19016  grpsubadd  19018  eqg0el  19173  gastacos  19300  orbsta  19303  lsslss  20934  prmirredlem  21458  zndvds  21543  zntoslem  21550  cygznlem1  21560  islindf2  21808  ismhp3  22133  coe1mul2lem1  22254  ply1chr  22294  restcld  23164  leordtvallem1  23202  leordtvallem2  23203  ist1-2  23339  xkoccn  23611  qtopcld  23705  ordthmeolem  23793  qustgpopn  24112  isxmet2d  24321  prdsxmetlem  24362  xblss2  24396  imasf1oxms  24486  neibl  24498  xrtgioo  24810  xrsxmet  24813  isncvsngp  25165  minveclem4  25448  minveclem6  25450  minveclem7  25451  mbfmulc2lem  25664  mbfmax  25666  mbfi1fseqlem4  25736  itg2gt0  25778  itg2cnlem2  25780  iblpos  25810  r1pid2  26186  logbgt0b  26818  angrteqvd  26831  affineequiv  26848  affineequiv2  26849  dcubic  26871  rlimcnp  26990  rlimcnp2  26991  efexple  27307  bposlem7  27316  lgsabs1  27362  lgsquadlem1  27406  m1lgs  27414  subadds  28074  lnhl  28539  colinearalg  28841  axcontlem2  28896  nbupgrel  29278  nb3grpr  29315  usgr0edg0rusgr  29509  isspthonpth  29683  rusgrnumwwlkl1  29899  eupth2lem3lem4  30161  minvecolem4  30810  minvecolem6  30812  minvecolem7  30813  hvmulcan2  31003  xppreima  32563  fzo0opth  32710  fracerl  33161  dvdsrspss  33268  ply1degltel  33468  r1pid2OLD  33482  smatrcl  33624  pstmxmet  33725  xrge0iifcnv  33761  ballotlemsima  34362  poimirlem27  37361  itg2addnclem  37385  itg2addnclem2  37386  iblabsnclem  37397  areacirclem2  37423  areacirclem4  37425  cvlcvrp  39051  ontric3g  43226  alephiso2  43262  sqrtcvallem1  43335  ntrclsk2  43772  ntrclsk13  43775  ntrneixb  43799  neicvgel1  43823  radcnvrat  44025  limsupmnflem  45377  dfvopnbgr2  47456  logbge0b  47987  affinecomb2  48127  line2x  48178  itscnhlc0yqe  48183