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  2544  necon2bbid  3000  notsep  5333  fressnfv  7157  eluniima  7248  dfac2b  10121  alephval2  10563  adderpqlem  10945  1idpr  11020  leloe  11302  negeq0  11518  addeq0  11643  muleqadd  11864  addltmul  12486  xrleloe  13175  fzrev  13622  mod0  13916  modirr  13985  cjne0  15221  lenegsq  15379  fsumsplit  15799  sumsplit  15826  dvdsabseq  16377  xpsfrnel  17622  isacs2  17715  acsfn  17721  comfeq  17768  sgrp2nmndlem3  18993  resscntz  19409  gexdvds  19660  hauscmplem  23574  hausdiag  23813  utop3cls  24419  affineequivne  27003  eqcuts2  27990  z12sge0  28687  ltgov  28877  ax5seglem4  29293  mdsl2i  32685  rspc2daf  32824  cycpmco2  33462  cntrval2  33500  pl1cn  34354  fineqvpow  35536  satefvfmla1  35925  bj-isrvec  37966  topdifinfeq  38024  finxpreclem6  38070  wl-sb8ft  38233  ftc1anclem5  38376  fdc1  38425  relcnveq  39005  relcnveq2  39006  elrelscnveq  39305  elrelscnveq2  39306  lcvexchlem1  39836  lkreqN  39972  glbconxN  40180  islpln5  40337  islvol5  40381  cdlemefrs29bpre0  41198  cdlemg17h  41470  cdlemg33b  41509  tfsconcat0i  44100  tfsconcat0b  44101  oadif1lem  44134  oadif1  44135  brnonrel  44343  frege92  44709  e2ebind  45300  stoweidlem28  46770  clnbupgrel  48627  0funcg2  49890