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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  sbco3  2513  necon2bbid  2985  notzfaus  5362  fressnfv  7158  eluniima  7249  dfac2b  10125  alephval2  10567  adderpqlem  10949  1idpr  11024  leloe  11300  negeq0  11514  addeq0  11637  muleqadd  11858  addltmul  12448  xrleloe  13123  fzrev  13564  mod0  13841  modirr  13907  cjne0  15110  lenegsq  15267  fsumsplit  15687  sumsplit  15714  dvdsabseq  16256  xpsfrnel  17508  isacs2  17597  acsfn  17603  comfeq  17650  sgrp2nmndlem3  18806  resscntz  19197  gexdvds  19452  hauscmplem  22910  hausdiag  23149  utop3cls  23756  affineequivne  26332  eqscut2  27307  ltgov  27848  ax5seglem4  28190  mdsl2i  31575  rspc2daf  31708  cycpmco2  32292  pl1cn  32935  fineqvpow  34096  satefvfmla1  34416  bj-isrvec  36175  topdifinfeq  36231  finxpreclem6  36277  ftc1anclem5  36565  fdc1  36614  relcnveq  37191  relcnveq2  37192  elrelscnveq  37362  elrelscnveq2  37363  lcvexchlem1  37904  lkreqN  38040  glbconxN  38249  islpln5  38406  islvol5  38450  cdlemefrs29bpre0  39267  cdlemg17h  39539  cdlemg33b  39578  tfsconcat0i  42095  tfsconcat0b  42096  oadif1lem  42129  oadif1  42130  brnonrel  42340  frege92  42706  e2ebind  43324  stoweidlem28  44744