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  8059  mapsnend  9048  adderpqlem  11020  mulerpqlem  11021  lesub2  11792  rec11  11996  fimaxre  12242  fiminre  12245  avglt1  12565  ixxun  13473  modmuladdnn0  14038  hashdom  14503  hashle00  14524  hashf1lem1  14580  swrdspsleq  14795  repsdf2  14909  2shfti  15213  mulre  15268  rlim  15642  rlim2  15643  modremain  16558  nn0seqcvgd  16725  divgcdcoprm0  16820  prmreclem6  17079  pwsleval  17645  issubc  17990  ismgmid  18825  grpsubeq0  19216  grpsubadd  19218  eqg0el  19378  gastacos  19504  orbsta  19507  lsslss  21216  prmirredlem  21758  zndvds  21835  zntoslem  21842  cygznlem1  21852  islindf2  22100  ismhp3  22443  coe1mul2lem1  22566  ply1chr  22604  restcld  23470  leordtvallem1  23508  leordtvallem2  23509  ist1-2  23645  xkoccn  23918  qtopcld  24012  ordthmeolem  24100  qustgpopn  24419  isxmet2d  24626  prdsxmetlem  24667  xblss2  24701  imasf1oxms  24788  neibl  24800  xrtgioo  25106  xrsxmet  25109  isncvsngp  25450  minveclem4  25733  minveclem6  25735  minveclem7  25736  mbfmulc2lem  25948  mbfmax  25950  mbfi1fseqlem4  26019  itg2gt0  26061  itg2cnlem2  26063  iblpos  26093  r1pid2  26460  logbgt0b  27103  angrteqvd  27116  affineequiv  27133  affineequiv2  27134  dcubic  27156  rlimcnp  27275  rlimcnp2  27276  efexple  27590  bposlem7  27599  lgsabs1  27645  lgsquadlem1  27689  m1lgs  27697  subadds  28438  lnhl  29063  elplng  29240  colinearalg  29470  axcontlem2  29525  nbupgrel  29908  nb3grpr  29945  usgr0edg0rusgr  30138  isspthonpth  30317  rusgrnumwwlkl1  30542  eupth2lem3lem4  30814  minvecolem4  31464  minvecolem6  31466  minvecolem7  31467  hvmulcan2  31657  xppreima  33221  fzo0opth  33377  fracerl  33850  dvdsrspss  33924  ply1degltel  34108  psrbasfsupp  34125  smatrcl  34410  pstmxmet  34511  xrge0iifcnv  34547  ballotlemsima  35131  poimirlem27  38533  itg2addnclem  38557  itg2addnclem2  38558  iblabsnclem  38569  areacirclem2  38595  areacirclem4  38597  cvlcvrp  40365  ontric3g  44481  alephiso2  44517  sqrtcvallem1  44590  ntrclsk2  45027  ntrclsk13  45030  ntrneixb  45054  neicvgel1  45078  radcnvrat  45257  limsupmnflem  46674  chnsubseqwl  47833  nprmmul1  48553  dfvopnbgr2  48895  pgnbgreunbgrlem2lem1  49156  pgnbgreunbgrlem2lem2  49157  logbge0b  49619  affinecomb2  49759  line2x  49810  itscnhlc0yqe  49815