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  5321  fressnfv  7135  eluniima  7227  dfac2b  10091  alephval2  10532  adderpqlem  10914  1idpr  10989  leloe  11267  negeq0  11483  addeq0  11608  muleqadd  11829  addltmul  12425  xrleloe  13111  fzrev  13555  mod0  13845  modirr  13914  cjne0  15136  lenegsq  15294  fsumsplit  15714  sumsplit  15741  dvdsabseq  16290  xpsfrnel  17532  isacs2  17621  acsfn  17627  comfeq  17674  sgrp2nmndlem3  18859  resscntz  19272  gexdvds  19521  hauscmplem  23300  hausdiag  23539  utop3cls  24146  affineequivne  26744  eqscut2  27725  zs12ge0  28349  ltgov  28531  ax5seglem4  28866  mdsl2i  32258  rspc2daf  32402  cycpmco2  33097  cntrval2  33135  pl1cn  33952  fineqvpow  35093  satefvfmla1  35419  bj-isrvec  37289  topdifinfeq  37345  finxpreclem6  37391  wl-sb8ft  37545  ftc1anclem5  37698  fdc1  37747  relcnveq  38317  relcnveq2  38318  elrelscnveq  38490  elrelscnveq2  38491  lcvexchlem1  39034  lkreqN  39170  glbconxN  39379  islpln5  39536  islvol5  39580  cdlemefrs29bpre0  40397  cdlemg17h  40669  cdlemg33b  40708  tfsconcat0i  43341  tfsconcat0b  43342  oadif1lem  43375  oadif1  43376  brnonrel  43585  frege92  43951  e2ebind  44560  stoweidlem28  46033  clnbupgrel  47839  0funcg2  49077