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  2516  necon2bbid  2973  notzfaus  5294  fressnfv  7103  eluniima  7194  dfac2b  10042  alephval2  10484  adderpqlem  10866  1idpr  10941  leloe  11221  negeq0  11437  addeq0  11562  muleqadd  11783  addltmul  12402  xrleloe  13084  fzrev  13530  mod0  13824  modirr  13893  cjne0  15114  lenegsq  15272  fsumsplit  15692  sumsplit  15719  dvdsabseq  16271  xpsfrnel  17515  isacs2  17608  acsfn  17614  comfeq  17661  sgrp2nmndlem3  18885  resscntz  19297  gexdvds  19548  hauscmplem  23359  hausdiag  23598  utop3cls  24204  affineequivne  26779  eqcuts2  27766  z12sge0  28463  ltgov  28653  ax5seglem4  28989  mdsl2i  32381  rspc2daf  32523  cycpmco2  33182  cntrval2  33220  pl1cn  34087  fineqvpow  35247  satefvfmla1  35595  bj-isrvec  37596  topdifinfeq  37654  finxpreclem6  37700  wl-sb8ft  37863  ftc1anclem5  38006  fdc1  38055  relcnveq  38637  relcnveq2  38638  elrelscnveq  38937  elrelscnveq2  38938  lcvexchlem1  39468  lkreqN  39604  glbconxN  39812  islpln5  39969  islvol5  40013  cdlemefrs29bpre0  40830  cdlemg17h  41102  cdlemg33b  41141  tfsconcat0i  43761  tfsconcat0b  43762  oadif1lem  43795  oadif1  43796  brnonrel  44004  frege92  44370  e2ebind  44978  stoweidlem28  46444  clnbupgrel  48298  0funcg2  49547