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  2511  necon2bbid  2968  notzfaus  5305  fressnfv  7098  eluniima  7190  dfac2b  10044  alephval2  10485  adderpqlem  10867  1idpr  10942  leloe  11220  negeq0  11436  addeq0  11561  muleqadd  11782  addltmul  12378  xrleloe  13064  fzrev  13508  mod0  13798  modirr  13867  cjne0  15088  lenegsq  15246  fsumsplit  15666  sumsplit  15693  dvdsabseq  16242  xpsfrnel  17484  isacs2  17577  acsfn  17583  comfeq  17630  sgrp2nmndlem3  18817  resscntz  19230  gexdvds  19481  hauscmplem  23309  hausdiag  23548  utop3cls  24155  affineequivne  26753  eqscut2  27735  zs12ge0  28378  ltgov  28560  ax5seglem4  28895  mdsl2i  32284  rspc2daf  32428  cycpmco2  33088  cntrval2  33126  pl1cn  33921  fineqvpow  35070  satefvfmla1  35397  bj-isrvec  37267  topdifinfeq  37323  finxpreclem6  37369  wl-sb8ft  37523  ftc1anclem5  37676  fdc1  37725  relcnveq  38295  relcnveq2  38296  elrelscnveq  38468  elrelscnveq2  38469  lcvexchlem1  39012  lkreqN  39148  glbconxN  39357  islpln5  39514  islvol5  39558  cdlemefrs29bpre0  40375  cdlemg17h  40647  cdlemg33b  40686  tfsconcat0i  43318  tfsconcat0b  43319  oadif1lem  43352  oadif1  43353  brnonrel  43562  frege92  43928  e2ebind  44537  stoweidlem28  46010  clnbupgrel  47819  0funcg2  49057