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  4742  opiota  8095  mapsnend  9092  adderpqlem  11066  mulerpqlem  11067  lesub2  11838  rec11  12042  fimaxre  12288  fiminre  12291  avglt1  12611  ixxun  13519  modmuladdnn0  14085  hashdom  14550  hashle00  14571  hashf1lem1  14627  swrdspsleq  14843  repsdf2  14957  2shfti  15262  mulre  15317  rlim  15691  rlim2  15692  modremain  16607  nn0seqcvgd  16774  divgcdcoprm0  16869  prmreclem6  17128  pwsleval  17694  issubc  18039  ismgmid  18874  grpsubeq0  19265  grpsubadd  19267  eqg0el  19427  gastacos  19554  orbsta  19557  lsslss  21266  prmirredlem  21808  zndvds  21885  zntoslem  21892  cygznlem1  21902  islindf2  22150  ismhp3  22493  coe1mul2lem1  22616  ply1chr  22654  restcld  23520  leordtvallem1  23558  leordtvallem2  23559  ist1-2  23695  xkoccn  23968  qtopcld  24062  ordthmeolem  24150  qustgpopn  24469  isxmet2d  24676  prdsxmetlem  24717  xblss2  24751  imasf1oxms  24838  neibl  24850  xrtgioo  25156  xrsxmet  25159  isncvsngp  25500  minveclem4  25783  minveclem6  25785  minveclem7  25786  mbfmulc2lem  25998  mbfmax  26000  mbfi1fseqlem4  26069  itg2gt0  26111  itg2cnlem2  26113  iblpos  26143  r1pid2  26510  logbgt0b  27151  angrteqvd  27164  affineequiv  27181  affineequiv2  27182  dcubic  27204  rlimcnp  27323  rlimcnp2  27324  efexple  27638  bposlem7  27647  lgsabs1  27693  lgsquadlem1  27737  m1lgs  27745  subadds  28486  lnhl  29111  elplng  29288  colinearalg  29518  axcontlem2  29573  nbupgrel  29956  nb3grpr  29993  usgr0edg0rusgr  30186  isspthonpth  30365  rusgrnumwwlkl1  30590  eupth2lem3lem4  30862  minvecolem4  31512  minvecolem6  31514  minvecolem7  31515  hvmulcan2  31705  xppreima  33311  fzo0opth  33465  fracerl  33938  dvdsrspss  34012  ply1degltel  34196  psrbasfsupp  34213  smatrcl  34498  pstmxmet  34599  xrge0iifcnv  34635  ballotlemsima  35218  poimirlem27  38757  itg2addnclem  38781  itg2addnclem2  38782  iblabsnclem  38793  areacirclem2  38819  areacirclem4  38821  cvlcvrp  40589  ontric3g  44715  alephiso2  44751  sqrtcvallem1  44823  ntrclsk2  45260  ntrclsk13  45263  ntrneixb  45287  neicvgel1  45311  radcnvrat  45490  limsupmnflem  46935  chnsubseqwl  48094  nprmmul1  48814  dfvopnbgr2  49156  pgnbgreunbgrlem2lem1  49417  pgnbgreunbgrlem2lem2  49418  logbge0b  49880  affinecomb2  50020  line2x  50071  itscnhlc0yqe  50076