Theorem bitr3di 286

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

Ref	Expression
bitr3di.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr3di.2	⊢ (𝜓 ↔ 𝜃)

Assertion

Ref	Expression
bitr3di	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Proof of Theorem bitr3di

Step	Hyp	Ref	Expression
1		bitr3di.2	. . 3 ⊢ (𝜓 ↔ 𝜃)
2	1	bicomi 224	. 2 ⊢ (𝜃 ↔ 𝜓)
3		bitr3di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	bitr2id 284	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  sbco3  2518  necon2bbid  2976  notzfaus  5309  fressnfv  7107  eluniima  7198  dfac2b  10045  alephval2  10487  adderpqlem  10869  1idpr  10944  leloe  11223  negeq0  11439  addeq0  11564  muleqadd  11785  addltmul  12381  xrleloe  13062  fzrev  13507  mod0  13800  modirr  13869  cjne0  15090  lenegsq  15248  fsumsplit  15668  sumsplit  15695  dvdsabseq  16244  xpsfrnel  17487  isacs2  17580  acsfn  17586  comfeq  17633  sgrp2nmndlem3  18854  resscntz  19266  gexdvds  19517  hauscmplem  23354  hausdiag  23593  utop3cls  24199  affineequivne  26797  eqscut2  27784  zs12ge0  28462  ltgov  28652  ax5seglem4  28988  mdsl2i  32380  rspc2daf  32522  cycpmco2  33196  cntrval2  33234  pl1cn  34093  fineqvpow  35252  satefvfmla1  35600  bj-isrvec  37470  topdifinfeq  37526  finxpreclem6  37572  wl-sb8ft  37726  ftc1anclem5  37869  fdc1  37918  relcnveq  38500  relcnveq2  38501  elrelscnveq  38800  elrelscnveq2  38801  lcvexchlem1  39331  lkreqN  39467  glbconxN  39675  islpln5  39832  islvol5  39876  cdlemefrs29bpre0  40693  cdlemg17h  40965  cdlemg33b  41004  tfsconcat0i  43623  tfsconcat0b  43624  oadif1lem  43657  oadif1  43658  brnonrel  43866  frege92  44232  e2ebind  44840  stoweidlem28  46308  clnbupgrel  48116  0funcg2  49365