Theorem syl5rbbr 275

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

Ref	Expression
syl5rbbr.1	⊢ (𝜓 ↔ 𝜑)
syl5rbbr.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5rbbr	⊢ (𝜒 → (𝜃 ↔ 𝜑))

Proof of Theorem syl5rbbr

Step	Hyp	Ref	Expression
1		syl5rbbr.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 214	. 2 ⊢ (𝜑 ↔ 𝜓)
3		syl5rbbr.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	syl5rbb 273	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  sbco3  2445  necon2bbid  2866  fressnfv  6467  eluniima  6548  dfac2  8991  alephval2  9432  adderpqlem  9814  1idpr  9889  leloe  10162  negeq0  10373  muleqadd  10709  addltmul  11306  xrleloe  12015  fzrev  12441  mod0  12715  modirr  12781  cjne0  13947  lenegsq  14104  fsumsplit  14515  sumsplit  14543  dvdsabseq  15082  xpsfrnel  16270  isacs2  16361  acsfn  16367  comfeq  16413  sgrp2nmndlem3  17459  resscntz  17810  gexdvds  18045  hauscmplem  21257  hausdiag  21496  utop3cls  22102  ltgov  25537  ax5seglem4  25857  mdsl2i  29309  addeq0  29638  pl1cn  30129  topdifinfeq  33328  finxpreclem6  33363  ftc1anclem5  33619  fdc1  33672  relcnveq  34234  relcnveq2  34235  elrelscnveq  34382  elrelscnveq2  34383  lcvexchlem1  34639  lkreqN  34775  glbconxN  34982  islpln5  35139  islvol5  35183  cdlemefrs29bpre0  36001  cdlemg17h  36273  cdlemg33b  36312  brnonrel  38212  frege92  38566  e2ebind  39096  stoweidlem28  40563