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  5309  fressnfv  7108  eluniima  7199  dfac2b  10046  alephval2  10488  adderpqlem  10870  1idpr  10945  leloe  11224  negeq0  11440  addeq0  11565  muleqadd  11786  addltmul  12382  xrleloe  13063  fzrev  13508  mod0  13801  modirr  13870  cjne0  15091  lenegsq  15249  fsumsplit  15669  sumsplit  15696  dvdsabseq  16245  xpsfrnel  17488  isacs2  17581  acsfn  17587  comfeq  17634  sgrp2nmndlem3  18855  resscntz  19267  gexdvds  19518  hauscmplem  23355  hausdiag  23594  utop3cls  24200  affineequivne  26798  eqcuts2  27787  z12sge0  28484  ltgov  28674  ax5seglem4  29010  mdsl2i  32402  rspc2daf  32544  cycpmco2  33219  cntrval2  33257  pl1cn  34125  fineqvpow  35284  satefvfmla1  35632  bj-isrvec  37512  topdifinfeq  37568  finxpreclem6  37614  wl-sb8ft  37768  ftc1anclem5  37911  fdc1  37960  relcnveq  38542  relcnveq2  38543  elrelscnveq  38842  elrelscnveq2  38843  lcvexchlem1  39373  lkreqN  39509  glbconxN  39717  islpln5  39874  islvol5  39918  cdlemefrs29bpre0  40735  cdlemg17h  41007  cdlemg33b  41046  tfsconcat0i  43665  tfsconcat0b  43666  oadif1lem  43699  oadif1  43700  brnonrel  43908  frege92  44274  e2ebind  44882  stoweidlem28  46349  clnbupgrel  48157  0funcg2  49406