Theorem 3bitr2d 299

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  ceqsralt  3446  raltpd  4535  opiota  7496  mapsnend  8307  adderpqlem  10098  mulerpqlem  10099  lesub2  10854  rec11  11056  avglt1  11603  ixxun  12486  modmuladdnn0  13016  hashdom  13465  hashle00  13484  hashf1lem1  13535  swrdspsleq  13746  repsdf2  13901  2shfti  14204  mulre  14245  rlim  14610  rlim2  14611  modremain  15512  nn0seqcvgd  15663  divgcdcoprm0  15758  prmreclem6  16003  pwsleval  16513  issubc  16854  ismgmid  17624  grpsubeq0  17862  grpsubadd  17864  gastacos  18100  orbsta  18103  lsslss  19327  coe1mul2lem1  20004  prmirredlem  20208  zndvds  20264  zntoslem  20271  cygznlem1  20281  islindf2  20527  restcld  21354  leordtvallem1  21392  leordtvallem2  21393  ist1-2  21529  xkoccn  21800  qtopcld  21894  ordthmeolem  21982  qustgpopn  22300  isxmet2d  22509  prdsxmetlem  22550  xblss2  22584  imasf1oxms  22671  neibl  22683  xrtgioo  22986  xrsxmet  22989  isncvsngp  23325  minveclem4  23607  minveclem6  23609  minveclem7  23610  mbfmulc2lem  23820  mbfmax  23822  mbfi1fseqlem4  23891  itg2gt0  23933  itg2cnlem2  23935  iblpos  23965  logbgt0b  24940  angrteqvd  24953  affineequiv  24970  affineequiv2  24971  dcubic  24993  rlimcnp  25112  rlimcnp2  25113  efexple  25426  bposlem7  25435  lgsabs1  25481  lgsquadlem1  25525  m1lgs  25533  lnhl  25934  colinearalg  26216  axcontlem2  26271  nbupgrel  26649  nb3grpr  26687  usgr0edg0rusgr  26880  isspthonpth  27058  rusgrnumwwlkl1  27304  eupth2lem3lem4  27604  minvecolem4  28287  minvecolem6  28289  minvecolem7  28290  hvmulcan2  28481  xppreima  29994  smatrcl  30403  pstmxmet  30481  xrge0iifcnv  30520  ballotlemsima  31119  poimirlem27  33979  itg2addnclem  34003  itg2addnclem2  34004  iblabsnclem  34015  areacirclem2  34043  areacirclem4  34045  cvlcvrp  35414  ntrclsk2  39205  ntrclsk13  39208  ntrneixb  39232  neicvgel1  39256  radcnvrat  39352  limsupmnflem  40745  logbge0b  43222  affinecomb2  43289  line2x  43320  itsclc0lem1  43322