Theorem syl5rbbr 278

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  sbco3  2535  necon2bbid  3013  fressnfv  6654  eluniima  6735  dfac2b  9238  dfac2OLD  9240  alephval2  9681  adderpqlem  10063  1idpr  10138  leloe  10413  negeq0  10626  muleqadd  10962  addltmul  11553  xrleloe  12221  fzrev  12654  mod0  12927  modirr  12993  cjne0  14241  lenegsq  14398  fsumsplit  14809  sumsplit  14835  dvdsabseq  15371  xpsfrnel  16535  isacs2  16625  acsfn  16631  comfeq  16677  sgrp2nmndlem3  17725  resscntz  18073  gexdvds  18309  hauscmplem  21535  hausdiag  21774  utop3cls  22380  ltgov  25841  ax5seglem4  26162  mdsl2i  29699  addeq0  30021  pl1cn  30510  topdifinfeq  33689  finxpreclem6  33724  ftc1anclem5  33970  fdc1  34022  relcnveq  34580  relcnveq2  34581  elrelscnveq  34729  elrelscnveq2  34730  lcvexchlem1  35048  lkreqN  35184  glbconxN  35392  islpln5  35549  islvol5  35593  cdlemefrs29bpre0  36410  cdlemg17h  36682  cdlemg33b  36721  brnonrel  38667  frege92  39020  e2ebind  39538  stoweidlem28  40977