Theorem bitr3di 289

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 227	. 2 ⊢ (𝜃 ↔ 𝜓)
3		bitr3di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	bitr2id 287	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  sbco3  2543  necon2bbid  2999  notsep  5334  fressnfv  7157  eluniima  7248  dfac2b  10113  alephval2  10556  adderpqlem  10938  1idpr  11013  leloe  11295  negeq0  11511  addeq0  11636  muleqadd  11857  addltmul  12479  xrleloe  13168  fzrev  13614  mod0  13908  modirr  13977  cjne0  15213  lenegsq  15371  fsumsplit  15791  sumsplit  15818  dvdsabseq  16370  xpsfrnel  17615  isacs2  17708  acsfn  17714  comfeq  17761  sgrp2nmndlem3  18986  resscntz  19402  gexdvds  19653  hauscmplem  23542  hausdiag  23781  utop3cls  24387  affineequivne  26968  eqcuts2  27955  z12sge0  28652  ltgov  28842  ax5seglem4  29248  mdsl2i  32640  rspc2daf  32779  cycpmco2  33419  cntrval2  33457  pl1cn  34311  fineqvpow  35482  satefvfmla1  35871  bj-isrvec  37882  topdifinfeq  37940  finxpreclem6  37986  wl-sb8ft  38149  ftc1anclem5  38292  fdc1  38341  relcnveq  38923  relcnveq2  38924  elrelscnveq  39223  elrelscnveq2  39224  lcvexchlem1  39754  lkreqN  39890  glbconxN  40098  islpln5  40255  islvol5  40299  cdlemefrs29bpre0  41116  cdlemg17h  41388  cdlemg33b  41427  tfsconcat0i  44020  tfsconcat0b  44021  oadif1lem  44054  oadif1  44055  brnonrel  44263  frege92  44629  e2ebind  45220  stoweidlem28  46690  clnbupgrel  48544  0funcg2  49807