Theorem bitr3di 289

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sbco3  2545  necon2bbid  3002  notsep  5329  fressnfv  7188  eluniima  7277  dfac2b  10236  alephval2  10684  adderpqlem  11066  1idpr  11141  leloe  11423  negeq0  11639  addeq0  11766  muleqadd  11987  addltmul  12609  xrleloe  13300  fzrev  13748  mod0  14043  modirr  14112  cjne0  15359  lenegsq  15517  fsumsplit  15936  sumsplit  15963  dvdsabseq  16512  xpsfrnel  17763  isacs2  17856  acsfn  17862  comfeq  17909  sgrp2nmndlem3  19153  resscntz  19577  gexdvds  19828  hauscmplem  23754  hausdiag  23994  utop3cls  24600  affineequivne  27185  eqcuts2  28202  z12sge0  28899  ltgov  29090  ax5seglem4  29540  mdsl2i  32954  rspc2daf  33135  cycpmco2  33764  cntrval2  33802  pl1cn  34657  fineqvpow  35883  satefvfmla1  36357  bj-isrvec  38407  topdifinfeq  38465  finxpreclem6  38511  wl-sb8ft  38674  ftc1anclem5  38807  findcard4  38824  fdc1  38872  relcnveq  39452  relcnveq2  39453  elrelscnveq  39752  elrelscnveq2  39753  lcvexchlem1  40283  lkreqN  40419  glbconxN  40627  islpln5  40784  islvol5  40828  cdlemefrs29bpre0  41645  cdlemg17h  41917  cdlemg33b  41956  tfsconcat0i  44539  tfsconcat0b  44540  oadif1lem  44573  oadif1  44574  brnonrel  44781  frege92  45147  e2ebind  45737  stoweidlem28  47243  clnbupgrel  49137  0funcg2  50404