Theorem syl5rbbr 274

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  sbco3  2405  necon2bbid  2825  fressnfv  6332  eluniima  6412  dfac2  8836  alephval2  9273  adderpqlem  9655  1idpr  9730  leloe  10003  negeq0  10214  muleqadd  10550  addltmul  11145  xrleloe  11853  fzrev  12273  mod0  12537  modirr  12603  cjne0  13751  lenegsq  13908  fsumsplit  14318  sumsplit  14341  dvdsabseq  14873  xpsfrnel  16046  isacs2  16137  acsfn  16143  comfeq  16189  sgrp2nmndlem3  17235  resscntz  17587  gexdvds  17822  hauscmplem  21019  hausdiag  21258  utop3cls  21865  ltgov  25292  ax5seglem4  25612  mdsl2i  28565  addeq0  28898  pl1cn  29329  topdifinfeq  32374  finxpreclem6  32409  ftc1anclem5  32659  fdc1  32712  lcvexchlem1  33339  lkreqN  33475  glbconxN  33682  islpln5  33839  islvol5  33883  cdlemefrs29bpre0  34702  cdlemg17h  34974  cdlemg33b  35013  brnonrel  36914  frege92  37269  e2ebind  37800  stoweidlem28  38921