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  2518  necon2bbid  2976  notzfaus  5338  fressnfv  7155  eluniima  7247  dfac2b  10150  alephval2  10591  adderpqlem  10973  1idpr  11048  leloe  11326  negeq0  11542  addeq0  11665  muleqadd  11886  addltmul  12482  xrleloe  13165  fzrev  13609  mod0  13898  modirr  13965  cjne0  15187  lenegsq  15344  fsumsplit  15762  sumsplit  15789  dvdsabseq  16337  xpsfrnel  17581  isacs2  17670  acsfn  17676  comfeq  17723  sgrp2nmndlem3  18908  resscntz  19321  gexdvds  19570  hauscmplem  23349  hausdiag  23588  utop3cls  24195  affineequivne  26794  eqscut2  27775  zs12ge0  28399  ltgov  28581  ax5seglem4  28916  mdsl2i  32308  rspc2daf  32452  cycpmco2  33149  pl1cn  33991  fineqvpow  35132  satefvfmla1  35452  bj-isrvec  37317  topdifinfeq  37373  finxpreclem6  37419  wl-sb8ft  37573  ftc1anclem5  37726  fdc1  37775  relcnveq  38345  relcnveq2  38346  elrelscnveq  38515  elrelscnveq2  38516  lcvexchlem1  39057  lkreqN  39193  glbconxN  39402  islpln5  39559  islvol5  39603  cdlemefrs29bpre0  40420  cdlemg17h  40692  cdlemg33b  40731  tfsconcat0i  43336  tfsconcat0b  43337  oadif1lem  43370  oadif1  43371  brnonrel  43580  frege92  43946  e2ebind  44555  stoweidlem28  46024  clnbupgrel  47815  0funcg2  49016