Theorem bitr3di 285

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 223	. 2 ⊢ (𝜃 ↔ 𝜓)
3		bitr3di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	bitr2id 283	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  sbco3  2518  necon2bbid  2988  notzfaus  5288  fressnfv  7026  eluniima  7117  dfac2b  9870  alephval2  10312  adderpqlem  10694  1idpr  10769  leloe  11045  negeq0  11258  addeq0  11381  muleqadd  11602  addltmul  12192  xrleloe  12860  fzrev  13301  mod0  13577  modirr  13643  cjne0  14855  lenegsq  15013  fsumsplit  15434  sumsplit  15461  dvdsabseq  16003  xpsfrnel  17254  isacs2  17343  acsfn  17349  comfeq  17396  sgrp2nmndlem3  18545  resscntz  18919  gexdvds  19170  hauscmplem  22538  hausdiag  22777  utop3cls  23384  affineequivne  25958  ltgov  26939  ax5seglem4  27281  mdsl2i  30663  rspc2daf  30795  cycpmco2  31379  pl1cn  31884  fineqvpow  33044  satefvfmla1  33366  eqscut2  33979  bj-isrvec  35444  topdifinfeq  35500  finxpreclem6  35546  ftc1anclem5  35833  fdc1  35883  relcnveq  36436  relcnveq2  36437  elrelscnveq  36589  elrelscnveq2  36590  lcvexchlem1  37027  lkreqN  37163  glbconxN  37371  islpln5  37528  islvol5  37572  cdlemefrs29bpre0  38389  cdlemg17h  38661  cdlemg33b  38700  brnonrel  41150  frege92  41516  e2ebind  42136  stoweidlem28  43523