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  5332  fressnfv  7160  eluniima  7250  dfac2b  10136  alephval2  10584  adderpqlem  10966  1idpr  11041  leloe  11323  negeq0  11539  addeq0  11664  muleqadd  11885  addltmul  12507  xrleloe  13197  fzrev  13644  mod0  13939  modirr  14008  cjne0  15252  lenegsq  15410  fsumsplit  15829  sumsplit  15856  dvdsabseq  16407  xpsfrnel  17652  isacs2  17745  acsfn  17751  comfeq  17798  sgrp2nmndlem3  19038  resscntz  19461  gexdvds  19712  hauscmplem  23632  hausdiag  23872  utop3cls  24478  affineequivne  27062  eqcuts2  28049  z12sge0  28746  ltgov  28937  ax5seglem4  29375  mdsl2i  32789  rspc2daf  32928  cycpmco2  33560  cntrval2  33598  pl1cn  34452  fineqvpow  35628  satefvfmla1  35991  bj-isrvec  38033  topdifinfeq  38091  finxpreclem6  38137  wl-sb8ft  38300  ftc1anclem5  38433  findcard4  38450  fdc1  38483  relcnveq  39063  relcnveq2  39064  elrelscnveq  39363  elrelscnveq2  39364  lcvexchlem1  39894  lkreqN  40030  glbconxN  40238  islpln5  40395  islvol5  40439  cdlemefrs29bpre0  41256  cdlemg17h  41528  cdlemg33b  41567  tfsconcat0i  44173  tfsconcat0b  44174  oadif1lem  44207  oadif1  44208  brnonrel  44416  frege92  44782  e2ebind  45373  stoweidlem28  46843  clnbupgrel  48737  0funcg2  49997