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  2512  necon2bbid  2969  notzfaus  5299  fressnfv  7088  eluniima  7179  dfac2b  10014  alephval2  10455  adderpqlem  10837  1idpr  10912  leloe  11191  negeq0  11407  addeq0  11532  muleqadd  11753  addltmul  12349  xrleloe  13035  fzrev  13479  mod0  13772  modirr  13841  cjne0  15062  lenegsq  15220  fsumsplit  15640  sumsplit  15667  dvdsabseq  16216  xpsfrnel  17458  isacs2  17551  acsfn  17557  comfeq  17604  sgrp2nmndlem3  18825  resscntz  19238  gexdvds  19489  hauscmplem  23314  hausdiag  23553  utop3cls  24159  affineequivne  26757  eqscut2  27740  zs12ge0  28386  ltgov  28568  ax5seglem4  28903  mdsl2i  32292  rspc2daf  32435  cycpmco2  33092  cntrval2  33130  pl1cn  33958  fineqvpow  35106  satefvfmla1  35437  bj-isrvec  37307  topdifinfeq  37363  finxpreclem6  37409  wl-sb8ft  37563  ftc1anclem5  37716  fdc1  37765  relcnveq  38335  relcnveq2  38336  elrelscnveq  38508  elrelscnveq2  38509  lcvexchlem1  39052  lkreqN  39188  glbconxN  39396  islpln5  39553  islvol5  39597  cdlemefrs29bpre0  40414  cdlemg17h  40686  cdlemg33b  40725  tfsconcat0i  43357  tfsconcat0b  43358  oadif1lem  43391  oadif1  43392  brnonrel  43601  frege92  43967  e2ebind  44575  stoweidlem28  46045  clnbupgrel  47844  0funcg2  49095