Theorem syl5rbbr 288

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 226	. 2 ⊢ (𝜑 ↔ 𝜓)
3		syl5rbbr.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	syl5rbb 286	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  sbco3  2555  necon2bbid  3061  notzfaus  5264  fressnfv  6924  eluniima  7011  dfac2b  9558  alephval2  9996  adderpqlem  10378  1idpr  10453  leloe  10729  negeq0  10942  addeq0  11065  muleqadd  11286  addltmul  11876  xrleloe  12540  fzrev  12973  mod0  13247  modirr  13313  cjne0  14524  lenegsq  14682  fsumsplit  15099  sumsplit  15125  dvdsabseq  15665  xpsfrnel  16837  isacs2  16926  acsfn  16932  comfeq  16978  sgrp2nmndlem3  18092  resscntz  18464  gexdvds  18711  hauscmplem  22016  hausdiag  22255  utop3cls  22862  affineequivne  25407  ltgov  26385  ax5seglem4  26720  mdsl2i  30101  rspc2daf  30233  cycpmco2  30777  pl1cn  31200  satefvfmla1  32674  topdifinfeq  34633  finxpreclem6  34679  ftc1anclem5  34973  fdc1  35023  relcnveq  35581  relcnveq2  35582  elrelscnveq  35734  elrelscnveq2  35735  lcvexchlem1  36172  lkreqN  36308  glbconxN  36516  islpln5  36673  islvol5  36717  cdlemefrs29bpre0  37534  cdlemg17h  37806  cdlemg33b  37845  brnonrel  39956  frege92  40308  e2ebind  40904  stoweidlem28  42320