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  2517  necon2bbid  2983  notzfaus  5362  fressnfv  7179  eluniima  7271  dfac2b  10172  alephval2  10613  adderpqlem  10995  1idpr  11070  leloe  11348  negeq0  11564  addeq0  11687  muleqadd  11908  addltmul  12504  xrleloe  13187  fzrev  13628  mod0  13917  modirr  13984  cjne0  15203  lenegsq  15360  fsumsplit  15778  sumsplit  15805  dvdsabseq  16351  xpsfrnel  17608  isacs2  17697  acsfn  17703  comfeq  17750  sgrp2nmndlem3  18939  resscntz  19352  gexdvds  19603  hauscmplem  23415  hausdiag  23654  utop3cls  24261  affineequivne  26871  eqscut2  27852  ltgov  28606  ax5seglem4  28948  mdsl2i  32342  rspc2daf  32486  cycpmco2  33154  pl1cn  33955  fineqvpow  35111  satefvfmla1  35431  bj-isrvec  37296  topdifinfeq  37352  finxpreclem6  37398  wl-sb8ft  37552  ftc1anclem5  37705  fdc1  37754  relcnveq  38324  relcnveq2  38325  elrelscnveq  38494  elrelscnveq2  38495  lcvexchlem1  39036  lkreqN  39172  glbconxN  39381  islpln5  39538  islvol5  39582  cdlemefrs29bpre0  40399  cdlemg17h  40671  cdlemg33b  40710  tfsconcat0i  43363  tfsconcat0b  43364  oadif1lem  43397  oadif1  43398  brnonrel  43607  frege92  43973  e2ebind  44588  stoweidlem28  46048  clnbupgrel  47826  0funcg2  48933